Page 37 - Textos de Matemática Vol. 40

1.5. Proof theory 25 (S-IN), (O-IN), or (N-IN) is proof-theoretically equivalent to primitive recursive
arithmetic PRA, and that BON + (Lp-IN) is equivalent to Peano arithmetic PA. Proposition 1.5.1. The following proof-theoretic equivalences hold:
1. BON+(S-IN)≡BON+(O-IN)≡BON+(N-IN)≡PRA. 2. BON + (Lp-IN) ≡ PA.
In fact, there is a straightforward translation ·N of the language LPA of Peano arithmetic into the language Lp which allows to prove a syntactical em- bedding of PA within BON + (Lp-IN), cf. [FJ93].
Following Cantini [Can96] and Ja¨ger and Strahm [JS95b], the above equivalences still hold in the presence of totality of application, (Tot), and ex- tensionality of operations, (Ext). In these cases formalized term model construc- tions serve to determine proof-theoretic upper bounds.
When we consider extensions of BON we will relate these extensions with theories of other frameworks, first of all subsystems of analysis or theories of inductive definition and fixed point theories. But before introducing these the- ories, we would like to discuss shortly the ordinal analysis which provides a uniform measure for mathematical theories, the proof-theoretic ordinal.
1.5.1 Ordinal analysis
In the beginning of the last century, Hilbert proposed a programme to show the consistency of formal theories by finitistic means. However, G¨odel’s Second Incompleteness Theorem shows that Hilbert’s programme cannot be realized in its original conception. When Gentzen proved the consistence of PA by means of transfinite induction for quantifier free formulae up to the ordinal ε0,5 [Gen36], he used a concept beyond purely finitary methods. But in this concept, the “transfiniteness” of a system is put into a mathematically clear notion which is—at least to some extent—constructively justified. Moreover, this approach allows one to give a uniform measure for mathematical theories, the so-called proof theoretic ordinal of a system.
An independent ordinal analysis needs two steps. For the lower bound, one has to carry out well-ordering proofs, while for the upper bounds cut-elimination procedures are used.
Usually, well-ordering proofs are rather technical and carrying out such a proof requires going up to the very limits of the axiom system. Examples for well-orderings proof may be found in [Buc75, BFPS81, BS88, Rat88, Set98, JKSS99]. In the context of explicit mathematics, well-ordering proofs are given by Ja¨ger and Strahm, [J¨ag83, JS96, Str99, Str02].
Cut-elimination can be performed in essentially two (not completely) dif- ferent ways, following Takeuti or Schu¨tte. A comparison of both methods may be found in [Buc97, Buc01].
5ε0 is the limit of ω powers, formally: ε0 := the least α such that α = ωα.