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(<epsilon_0)-recursion).  This led to the study of systems of
finite type which still allow to formalize substantial parts of
analysis, but which also guarantee the extractability of primitive
recursive, elementary recursive and even polynomial data.

In this talk we

  discuss the range and limits of polynomially bounded analysis PBA,

  the range and limits of PRA-reducible analysis PRedA detecting a
  precise borderline between fragments of analysis which are
  PRA-conservative and analytical principles which just go beyond the
  strength of PRA,

  introduce a new PA-conservative extension (of a finite type version
  of) ACA_0 which is based on strong principles of uniform
  boundedness.


S. Simpson

Predicativity: the outer limits

Beginning with ideas of Poincare and Weyl, Feferman in the sixties
undertook a profound analysis of the predicativist foundational
program.  He presented a subystem of second order arithmetic IR and
argued convincingly that it represents the outer limits of what is
predicatively provable.  Much later, Friedman introduced another
system ATR_0 which is conservative over IR for Pi^1_1 sentences yet
includes several well known theorems of algebra, descriptive set
theory, and countable combinatorics that are not provable in IR.  The
proof-theoretic ordinal of both systems is Gamma_0.  ATR_0 has emerged
as one of a handful of systems that are important for reverse
mathematics.  From a foundational standpoint, we may say that IR
represents predicative provability while ATR_0 represents predicative
reducibility.  Subsequently Friedman formulated mathematically natural
finite combinatorial theorems that are not only not predicatively
provable but go beyond Gamma_0 and therefore are not predicatively
reducible.  I plan to report on recent developments in this area.


M. Rathjen

Monotone inductive definitions in explicit mathematics 

The framework of Feferman's theory of explicit mathematics is
particularly suited to consider general constructive operations on
sets and their inductively defined fixed points. The talk will give a
survey of research on least fixed point axioms in explicit
mathematics.


A. Cantini

On extensionality, uniformity and comprehension in explicit
mathematics

The informal intuitions behind Feferman's explicit mathematics
naturally hint at a radically non-extensional ontology.  In
particular, there is a tension between uniform class comprehension and
class extensionality.

This is exemplified by a few negative results, which lift recursion
theoretic techniques to applicative theories of operations and
classes, and imply formal refutations of class extensionality and
power class existence.

On the positive side, we show that class extensionality is consistent
with non-trivial principles of uniform comprehension, (and yet it
forces simple class constructors, e.g. singleton, not to be uniformly
given by an internal operation).  The basic idea is to apply
Feferman's method for generating partial combinatory algebras to
models of provably consistent fragments of Quine's NF.


I. Mason / C. Talcott

Feferman-Landin logic 

In a series of papers in the 1960s Landin proposed that programming
languages should consist of the lambda calculus augmented by
primitives for manipulating data as well as aspects of a program's
environment such as state, control, or interactivity.  We will call
such languages ``Landinesque languages''.

In the 1970s and 1980s Feferman developed several theories for natural
formalization of constructive mathematics.  These theories treat
functions as objects in a first-order setting.

In the 1990s Mason, Talcott and their collaborators used Feferman's
theories as a starting point for developing formalisms for reasoning
about two specific Landinesque languages: IOCC (Impredicative theory
of Operations, Control, and Classes) and VTLoE (Variable Type Logic of
Effects).  The Landinesque language of IOCC incorporated a control
facility similar to Scheme's call/cc, while VTLoE incorporated ML-like
reference cells.

Following Feferman's ideas, both formalisms are essentially
first-order, two-layered theories.  The lower layer is a theory of
program equivalence.  The upper layer is a theory of class membership
with a general comprehension principle for defining classes.  Many
standard class constructions and data-types can be represented
naturally including algebraic abstract data types, list-, record-, and
function- type constructions.  In addition classes can be constructed
as minimal or maximal fix-points, which in turn give rise to
associated induction and co-induction principles.

More recently Talcott introduced a general framework for defining the
semantics of Landinesque languages along with the notion of uniform
semantics.  For such languages we have the combined benefits of
reduction calculi (modular axiomatization), and operational
equivalence (more equations).  In addition we have a sound basis for
defining satisfaction for VTLoE-style assertions.

In this talk we show how to combine all of these ideas in a logic for
reasoning about Landinesque languages called Feferman-Landin logic
(FLL for short).  FLL generalizes VTLoE to Landinesque languages with
uniform semantics.  We will give some examples of primitive operations
and their formalization in FLL and illustrate some of the subtilties
of reasoning about effects as well as the wide range of properties the
can be expressed in this logic.


C. Parsons

Reflections on predicativity 

Solomon Feferman's classic analysis of predicative provability,
together with the more or less parallel work of Schutte, brought to a
sort of closure the debates about predicativity that were inaugurated
at the beginning of the century by Poincare.

Some remarks will be made about the history of these debates, which
included the very dramatic expressions of concern about
impredicativity by Weyl and the defense of such methods on realist
grounds by several writers, most decisively Godel. It is hoped that
attention can also be paid to issues left over after the work up
through the 60's, impredicative specification of sets by
quantification over the universe, and the claim of the author and
others that the concept of natural number is impredicative.


J. Dawson

The unity of mathematics -- a foundational touchstone? 

This talk will address the issues: How has the oft-extolled unity of
mathematics been construed by philosophers and practitioners? How well
do familiar philosophies of mathematics account for such unity? And
are there obstacles to proof-theoretic criteria for distinguishing
different proofs of the ``same'' theorem?











J. FenstadComputability theory: structure or algorithms? 

In his paper ``Turing's ``oracle'': From absolute to relative computability -
and back'' S.Feferman discusses some major trends in recent work on degrees
of unsolvability, theories of recursive functionals and generalized
recursion theory and notes how ``marching in under the banner of degree
theory, these stands were to some extent woven together by the recursion
theorists, but the trend has been to pull the subject of effective
computability even farther away from questions of actual computation''.

Feferman had expressed similar concerns in a paper from 1977 ``Inductive
schemata and recursively continous functionals'', and both he and
Y.Moschovakis have sice pursued a programme of how to use ``abstract
recursion as a foundation for the theory of algorithms'' (to quote the title
of a paper of Moschovakis from 1984).

I had commented on this development in the introductory part of ``General
Recursion Theory'' from 1980, and I shall in this lecture start from this
point, briefly reviewing some developments at that time in axiomatic
recursion theory (computation theories) and fap-computability, paying
particular attention to both structural and algorithmic concerns.

The main part of my lecture will be devoted to current developments in
computability theories on many-sorted algebras, which generalises earlier
work on fap-computability; see the forthcoming survey by J.V.Tucker and
J.I.Zucker ``Computable functions and semicomputable sets on many-sorted
algebras'' (to appear in vol.5 of The Handbook of Logic in Computer
Science). I will indicate how this approach unifies a number of
developments in ``real'' computability, in particular, how it relates to the
recent work of S.Smale (see the book by Blum, Cucker, Shub and Smale, 1998)
on computation and complexity over the reals. I will conclude with some
remarks on computability over the non-standard reals.


T. StrahmReflective closures of formal systems 

The foundational program to study the principles of proof and ordinals
which are implicit in given concepts was first spelled out by Kreisel.
A paradigmatic example in this respect is the analysis of
predicativity by Feferman and Schutte in the early sixties, which led
to the progression of systems of ramified analysis up the the famous
Feferman-Scutte ordinal . Since then various means of
extending a formal system by principles which are implicit in its
axioms have been proposed and pushed forward by Feferman.

In this talk we survey different notions of reflective closure.  This
includes the discussion of numerous characterizations of
predicativity, the reflective closure of axiom systems by means of a
self-applicative truth predicate as well as Feferman's most recent
concept of unfolding a schematic formal system.  Special emphasis is
put on characterizing the reflective closure of specific systems in
more familiar proof-theoretic terms.