The symposium is centered around proof theoretically inspired
foundational investigations that have been merging over the last decades
with developments in set theory and recursion theory; however, they have
sustained a special emphasis on broad philosophical issues. Feferman's
primary contributions have been to proof theory, computation theory and,
in more recent years, to an analysis of the development of mathematical
logic in the twentieth century. Indeed, all of these matters are of
intense interest in the current discussion concerning modern
mathematical thought. The following paragraphs describe the main themes
for the symposium.
Proof theoretic ordinals
The most distinctive aspect of Gentzen's consistency proof for
elementary arithmetic was the use of quantifier-free transfinite induction
up to the first epsilon number, epsilon0. Ever since the construction of
effective systems of ordinal notations has been a significant, for some the
central, part of proof theoretic investigations. Feferman and Schütte
contributed decisively already in the sixties, when characterizing the
limits of predicativity involving the ordinal Gamma0. Feferman's
proposals for intelligible principles for the construction of stronger
notation systems and their use in the investigation of subsystems of
analysis, inspired in the mid-seventies the work of Buchholz and Pohlers.
Partially also following Takeuti's lead, they determined the proof theoretic
ordinals of impredicative subsystems of analysis. Rathjen, a student of
Pohlers, has obtained the strongest results in this direction; Sommer has
been exploring a more model-theoretic approach to such notation systems.
Foundational reductions
The use of (quantifier-free) transfinite induction along proof theoretic
ordinals is motivated by an extension of Hilbert's program: to prove the
consistency of classical theories for analysis with appropriate
constructive , not just finitist, means. However, there are ways of
giving consistency proofs relative to other constructively acceptable
theories: reductions to constructive higher number classes, versions of
Gödel's Dialectica interpretation involving systems of computable
functionals, various type theories including those developed by
Martin-Löf. Prawitz has investigated such constructive theories; Avigad
has used extensions of the Dialectica interpretation for the treatment
of fairly strong classical theories. Finally, Feferman's systems of
explicit mathematics (with intuitionistic logic) are viewed also as base
constructive theories. The philosophical point of course is that the
constructive theories have a distinguished epistemological status.
Formalization in restricted systems
The attempt to establish the consistency of stronger and stronger
classical theories was accompanied by the systematic development of
analysis in weaker and weaker formal theories. In the late seventies, a
real turning point was reached: all of classical analysis, as Takeuti
showed, can be developed in a system that is conservative over
elementary number theory. Feferman and Friedman obtained similarly
sweeping results; that led to the investigation of which weaker systems
were still sufficient for which parts of mathematics. This is part of a
more systematic enterprise that was pushed along by Friedman and Simpson
under the name Reverse Mathematics ; here one wants to show, roughly
speaking, which set existence principles are needed for, i.e. are
equivalent to, particular mathematical theorems. Constable has been
implementing constructive theories, like Martin-Löf's type theory, to
allow for interactive theorem proving; Kohlenbach has been exploiting
formalizability in weak theories to extract computational information
from proofs.
Applicative and self-applicative theories
In 1967, Bishop's book Foundations of Constructive Mathematics
created a stir by pioneering a constructive version of mathematics that
could co-exist with classical mathematics. Feferman's applicative theories
were put forward in 1975 as natural theories in which to formalize Bishop's
work. They grew naturally out of his work on generalized recursion theory,
in which the interpretation of "operations" might be recursive functions or
functions from some generalized (non-recursive) class. Applicative theories
have been extensively studied (e.g. by Beeson, Buchholz, Glass, Jäger,
Kahle, Pohlers, Sieg, Strahm, and Tatsuta), and have also served as a basis
for the axiomatization of certain ideas in mathematical philosophy, such as
the theory of Frege structures (e.g. by Beeson, Hayashi and Kobayashi, and
Kahle). The work on applicative theories has implications for and
applications in: foundations of mathematics in general; foundations of
constructive mathematics in particular; proof theoretical analyses of the
strength of axiom systems; computer science (correctness and termination of
algorithms; polymorphism).
Generalized computation and reflective closure
The study of generalized computation arose as an attempt to extend the
classical theory of computation from the natural numbers to other
domains. The leaders in the early days of this work were Feferman,
Kreisel, Kripke, Levy, Moschovakis, Platek, Sacks, and Takeuti. The aim
was several fold. In part one wanted to understand the classical theory
better by seeing which aspects of the theory generalized to various
kinds of domains. A second aim was to fit the theory of computation into
a general theory of definability. A third aim was to develop a set of
tools that could be used in other parts of mathematical logic, set
theory (Karp and Jensen), model theory (Barwise), and proof theory
(Feferman, Tait, followed by a host of others). -- The second topic of
this section (initially strongly related to the classical theory of
computation via progressions of theories and autonomous versions thereof)
is Feferman's study of the reflective closure of theories, a process
whereby ideas implicit in a theory but going beyond it formally are
extracted as additional premises for a stronger theory.
Philosophy and history of modern mathematical logic
The emphasis here is on themes brought out and discussed in the earlier
sessions, but with a more distinctively philosophical eye and a broader
historical perspective. There are, most importantly, the roots for
Hilbert's and Gödel's work. Those for Hilbert go back to the
foundational discussions between Kronecker, Dedekind, and Cantor.
Hilbert's way of formulating sharp (meta) mathematical problems is
certainly a most important context for Gödel's pathbreaking work. How
sympathetic Gödel was to an expanded version of Hilbert's program has
become evident only through the publication of previously unpublished
material in volume III of Gödel's Collected Works. Feferman's
editorship of these Collected Works
has been accompanied by analyses of
the broader aspects of Gödel's thought; e.g., the search for and the
justification of new axioms. Parsons, Dawson, and Sieg are also
involved in the edition of the Collected Works and have written
extensively about historical developments of modern mathematical logic
and provided philosophical analyses. Tait has done important work in
proof theory and contributed significantly to the philosophy of
mathematics. As mentioned above, proof theoretic investigations have
sustained more clearly than other foundational enterprises a deep
philosophical component.