Reflections

Symposium themes

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.