Gödel’s program for new axioms: Why, where, how and what? (English) Zbl 0857.03034

Feferman, Solomon

Hájek, Petr (ed.), Gödel ’96. Logical foundations of mathematics, computer science and physics – Kurt Gödel’s legacy. Proceedings of a conference, Brno, Czech Republic, August 1996. Berlin: Springer-Verlag. Lect. Notes Log. 6, 3-22 (1996).

In seeking to extend our present axiom systems for mathematics, the author proposes precise ways of doing so that obey Gödel’s suggestion that the new axioms be “exactly as evident” as those already accepted. Starting from a system with given formal schemata for axioms and rules of inference, he defines an enlarged system that he calls the ‘unfolding’ of the original system and that is supposed to yield all that should be accepted if the concepts and principles of the given system are accepted. This is done in some detail for a version NFA of non-finitist arithmetic. The first step constructs the operational unfolding \({\mathcal U}_o(\text{NFA})\), in which new operations are introduced by an axiomatic version of Moschovakis’s generalized recursion theory (with partial functions and functionals of type level \(\leq 2)\), and with Beeson’s logic of partial terms as the underlying logic. \({\mathcal U}_o \text{(NFA)}\) turns out to be a conservative extension of PA that is proof-theoretically equivalent to PA. The second step defines the full unfolding \({\mathcal U} \text{(NFA})\) that adds a type for propositions and treats predicates as propositional functions (in the style of Aczel’s Frege structures). Together with Thomas Strahm, the author has shown that \({\mathcal U} \text{(NFA)}\) is a conservative extension of the system of ramified analysis up to but not including \(\Gamma_0\) and is proof-theoretically equivalent to that system. The unfolding of a suitable functional system ST for ZF set theory is only sketched and some results are described for the operational and full unfolding of a subsystem AST for admissible set theory. The strength of an unfolding depends strongly on the basic set theory. For example, if we add to ST the downward reflection principle (D-Ref): \(P\to\exists b [a\in b\wedge\text{Trans} (b)\wedge P^{(b)}]\), then the existence of hierarchies of Mahlo cardinals can be obtained in the unfolding, but the author argues that we cannot obtain a breakthrough in this way with respect to stronger large cardinals (such as measurable cardinals) and that this is a confirmation of intuitions expressed by Tarski and Gödel.
For the entire collection see [Zbl 0844.00017].

Reviewer: E.Mendelson (Flushing)

MSC:

03F35	Second- and higher-order arithmetic and fragments
03E70	Nonclassical and second-order set theories
03E55	Large cardinals
03F15	Recursive ordinals and ordinal notations
03D65	Higher-type and set recursion theory
03D75	Abstract and axiomatic computability and recursion theory

Keywords:

higher-order arithmetics; higher-order set theory; extension of ramified analysis; functional system for ZF set theory; unfolding of a subsystem for admissible set theory; axiom systems for mathematics; non-finitist arithmetic; operational unfolding; axiomatic version of Moschovakis’s generalized recursion theory; Beeson’s logic of partial terms; conservative extension of PA; full unfolding; hierarchies of Mahlo cardinals; large cardinals