Ordinal analysis without proofs

Summary

Abstract. An approach to ordinal analysis is presented which is finitary, but highlights the semantic content of the theories under consideration, rather than the syntactic structure of their proofs. In this paper the methods are applied to the analysis of theories extending Peano arithmetic with transfinite induction and transfinite arithmetic hierarchies.

Introduction. As the name implies, in the field of proof theory one tends to focus on proofs. Nowhere is this emphasis more evident than in the field of ordinal analysis, where one typically designs procedures for “unwinding” derivations in appropriate deductive systems. One might wonder, however, if this emphasis is really necessary; after all, the results of an ordinal analysis describe a relationship between a system of ordinal notations and a theory, and it is natural to think of the latter as the set of semantic consequences of some axioms. From this point of view, it may seem disappointing that we have to choose a specific deductive system before we can begin the ordinal analysis.

In fact, Hilbert's epsilon substitution method, historically the first attempt at finding a finitary consistency proof for arithmetic, has a more semantic character. With this method one uses so-called epsilon terms to reduce arithmetic to a quantifier-free calculus, and then one looks for a procedure that assigns numerical values to any finite set of closed terms, in a manner consistent with the axioms. The first ordinal analysis of arithmetic using epsilon terms is due to Ackermann [1]; for further developments see, for example, [20].

More recently, investigations of nonstandard models of arithmetic due to Paris and Kirby have given rise to another approach, which incorporates Ketonen and Solovay's finitary combinatorial notion of an α-large set of natural numbers. Roughly speaking, to show that the proof-theoretic ordinal of a theory T is bounded by α, one uses an α-large interval in a nonstandard model of arithmetic to construct a model of T. These methods are surveyed and extended in [3, 4]; some of the constructions found in the second paper are derived from modeltheoretic methods due to Friedman [12, 13]. Sommer [28] has shown that one can avoid references to nonstandard models and instead view the methods as providing a way of building “finite approximations” to models of arithmetic, an idea which traces its way back to Herbrand [18].