Page 36 - Textos de Matemática Vol. 40

24 Chapter 1. Applicative theories
For more details about CT T we refer to [JS95b, Can96]. Later on, our model constructions for truth theories will mainly be based on CT T .
Extensionality. In both models, CN T and CT T , extensionality, (Ext), does not hold. In [Bee85] there are also discussed variants of CN T and CT T , in where the universe consists of all terms (not only closed ones). Based on these models, it is possible to form normal as well as total term models which satisfy (Ext) by including η reduction rules in the reduction relation, cf. [Bee85, Section VI.6.3 and VI.6.4].
1.5 Proof theory
Considering theories with mathematical content, it is a natural question to ask for the expressive power of these theories. Measuring mathematical expressive- ness of a theory is a topic of proof theory, in particular, in its branch dealing with ordinal analysis. The classical references for proof theory are Hilbert and Bernays [HB34, HB39] as well as Kleene [Kle52]. Modern proof theory is de- scribed in the monographs of Schu¨tte [Sch60, Sch77] and Takeuti [Tak87]3. While Girard’s monograph [Gir87] serves as a good reference for a more ad- vanced reader, the lecture notes of Pohlers is very suitable as an introduction. Besides the excellent Handbook of Mathematical Logic [Bar77], the Handbook of Proof Theory, edited by Buss, [Bus98] contains important contributions. Fo- cusing on ordinal analysis, Pohlers has written a series of papers which serve as references, [Poh82, Poh86, Poh91, Poh92, Poh96, Poh98]. Also the papers [Rat98b, Rat99b, Rat06] of Rathjen provide excellent introductions and sur- veys. For further pointers to the literature we refer to the extensive references in [Poh89] and [Rat99b].
For a more detailed discussion of ordinal analysis, in particular for the core of so-called reductive proof-theory, we refer to Feferman [Fef88a] and [Fef00]. There, a precise definition of proof theoretic reduction is given and compared with the related notions from model theory (in the first paper) and the notions of translation and relative interpretations (in the latter one). Roughly speaking, a proof-theoretic reduction is given by a partial recursive function from the proof of a theory T to the proofs of a theory S which preserves proofs of a certain class of formulae Φ. In particular, Φ has to contain absurdity, so that the reduction ensures relative consistency. Finally, the proof of these properties has to be carried out by “elementary” means. Usually, primitive recursive arithmetic, PRA, is chosen for this aim.4
Proof Theory of BON. For the basic theory BON the situation is easy. It is known from [FJ93] and [Str96a] that BON plus anyone of the induction principles
3The second edition of Takeuti’s book extends the first edition from 1975 by additional contributions from other leading proof theorists.
4In [Fef88a], Feferman proposed to use the theory S to prove these properties. Unfortu- nately, an example due to Niebergall shows that this definition is not transitive.