REFLECTIONS
A Symposium Honoring Solomon Feferman
on his 70th Birthday
December 11-13 1998, Stanford University
Organizing Committee:
Jon Barwise (co-chair), Wilfried Sieg (co-chair),
Rick Sommer, Carolyn Talcott
This symposium (a.k.a. the Feferfest) is centered around proof
theoretically inspired foundational investigations. Solomon Feferman
has been a contributor to these investigations during the last forty
years in a most systematic and significant way, and the main themes of
the Symposium are themes in his work. The Symposium is a tribute to
him on the occasion of his 70-th birthday -- a tribute both to his
specific contributions and to his influence on the direction of
current research.
Program
Note that the last 10 minutes of each talk is reserved for questions
and for Sol to have a chance to contribute to the discussion.
*December 11; 100 Cordura Hall
9:30 Opening remarks. J. Barwise
*Session I: Proof theoretic ordinals (Chair: G. Mints)
[9:45]
W. Pohlers; Proof-theoretic ordinals for theories in the language of
(second order) arithmetic and set theory
[10:45] Break
[11:00] J. Avigad; Ordinal analysis without proofs
[11:45] R. Sommer; Iterating reflection
[12:30] Lunch
*Session II: Foundational reductions (Chair: W. Sieg)
[2:00] P. Martin-Lof; Modelling versus Tarski semantics.
[3:00] J. Barwise; Symbolic and presymbolic logic
[3:45] Break
[4:00] J. van Bentham; Logical constants: the variable fortunes of an
elusive notion
[4:45] End of session
[7:00] Reception/buffet
*December 12; Gates Building, B03
*Session III: Formalizations in restricted systems
(Chair: S. Buss)
[9:30] G. Takeuti; Godel sentences of bounded arithmetic
[10:30] R. Constable; Admiring proof reflections and working with them
[11:15] Break
[11:30] U. Kohlenbach; Classical analysis in weak systems of finite type
[12:15] S. Simpson; Predicativity: the outer limits
[1:00] Lunch
*Session IV: Applicative and self-applicative theories
(Chair: M. Beeson)
[2:00] D. Scott; Project update: logics of types and computations
[3:00] M. Rathjen; Monotone inductive definitions in
explicit mathematics
[3:45] Break
[4:00] A. Cantini; On extensionality, uniformity and comprehension in
explicit mathematics
[4:45] I. Mason/ C. Talcott; Feferman-Landin logic
[5:30] End of session
[7:00PM] BANQUET at the Stanford Faculty Club
*December 13; Gates Building, B03
*Session V: Philosophy and history of modern mathematical thought
(Chair: D. Follesdal)
[9:30] C. Parsons; Reflections on predicativity
[10:30] J. Dawson; The unity of mathematics -- a foundational touchstone?
[11:15] Break
[11:30] W. Sieg; TBA
[12:15] W. Tait; Some remarks about finitism
[1:00] Lunch
*Session VI: Generalized computation and reflective closure
(Chair: J. Etchemendy)
[2:00] S. Wainer; Accessible recursive functions
[3:00] J. Fenstad; Computability theory: structure or algorithms?
[3:45] Break
[4:00] T. Strahm; Reflective closures of formal systems
[4:45] Closing remarks: W. Sieg
Abstracts
W. Pohlers
Proof-theoretic ordinals for theories in the language of (second
order) arithmetic and set theory
We give a survey on the ordinal analysis of theories in the language
of arithmetic and set theory with emphasis on impredicative theories.
R. Sommer
Iterating reflection
In the spirit of ``Reflections,'' the title of this symposium, I will
reflect on some of Feferman's work on iterating reflection principles
(i.e., statements asserting that provable statements are true). A
brief history of the work of Turing and Feferman on this topic will
pave the way for presentation of more recent results in this area.
Feferman's contribution extends Turing's and demonstrates that all of
true arithmetic can be captured by iterating reflection principles
along the recursive well orderings. Schmerl later showed that starting
with PRA and then iterating -reflection along fixed notation systems
gives a fine structure of theories, and that standard axiom systems,
such as Peano Arithmetic, are captured at precise levels along the
way. My results show that the metamathematically defined theories of
iterated reflection are equivalent to purely mathematical ones. In
particular, I show that the hierarchy of statements generated by
iterated -reflection, starting with Elementary Recursive Arithmetic,
corresponds exactly to statements of totality of functions in the
fast-growing hierarchy. By relativizing the fast-growing hierarchy to
functions recursive in a -complete set, we obtain all of the levels of
Schmerl's -reflection hierarchies for . Since model-theoretic ordinal
analysis gives explicit characterizations of the provable functions of
theories in terms of the functions in these hierarchies, recent
results in this area serve to locate many of the standard predicative
theories in hierarchies of iterated reflection.
J. Barwise
Symbolic and presymbolic logic
Real world embedded systems have to reason with information in a
variety of forms. In recent years, a number of researchers have
developed so-called ``hybrid systems'' for reasoning with such
information. Many of these systems are rather ad hoc, responding to
the needs of some artificial system like a robot. In this talk I will
sketch a principled approach to hybrid reasoning and illustrate it
with a system implemented in Mathematica. The system grew out of
ideas in my 1997 book with Jerry Seligman, ``Information Flow: The
logic of distributed systems.''
G. Takeuti
Godel sentences of bounded arithmetic
In his early work, Feferman emphasized that the arithmetization of
metamathematics must be carried out intensionally. Bounded Arithmetic
is a very interesting case in this sense. We present two
formalizations of proof predicate of Bounded Arithmetic. One of them
is the usual proof predicate and another one gives a detailed
information on bounds of free variables used in the proof. Now
Bounded Arithmetic has the following special feature of Godel
sentences. Even if we fix one formalization of proof predicate, it
has infinitely many Godel sentences and their properties and their
mutual relations are closely related to the problem. Therefore the
study of Godel sentences of Bounded Arithmetic is an excellent
approach to the problem. In our two formalizations of proof predicate
of Bounded Arithmetic we show that the properties of their Godel
sentences form a good contrast to each other and discuss how problem
is related to their properties.
R. Constable
Admiring proof reflections and working with them
This talk will discuss the role of reflection in the work of reasoning
about programs and protocols using a proof development system such as
Nuprl. The talk discusses the kind of proof really used in
applications. They are called tactic-tree proofs. The talk discusses
the role of reflection in specifying the computational complexity of
programs synthesized from constructive proofs. I note several points
at which Sol Feferman's results have shaped the design of Nuprl.
U. Kohlenbach
Classical analysis in weak systems of finite type
In the 70s S. Feferman introduced a mathematically strong system S =
restricted(PA^omega) + QF-AC + mu for classical mathematics (and in
particular analysis) and showed that S is conservative over Peano
arithmetic PA. S is formulated in the language of arithmetic in all
finite types (with induction restricted to arithmetical formulas) and
based on a non-constructive mu-operator. The conservation proof uses
Godel's functional interpretation relative to mu.
In this talk we survey some of our work which was stimulated by
Feferman's paper: systems in the language of finite types allow a
rather direct formalization of important analytical concepts and
functional interpretation, because of its good behaviour with respect
to the logical deduction rules (`modularity'), is a very useful tool
to extract constructive data out of given proofs. For these data to
be of mathematical relevance it is important to keep their numerical
complexity low (in particular well below general
alpha(