Page 39 - Textos de Matemática Vol. 40

1.5. Proof theory 27
Thetheories(Π1-CA)0,(Π1-CA)<ωω,and(Π1-CA)<ε0 whichareusedinthe proof-theoretic results for the Suslin operator in Section 1.6.2 may be found, for instance, in [JS02a, Section 3.1].
For a comprehensive presentations of the proof-theoretic results and meth- ods for subsystems of analysis we refer to Pohlers’s Handbook article [Poh98] and the monograph of Buchholz and Schu¨tte [BS88].
Reverse mathematics. A special branch of this area is reverse mathe- matics. In this programme started by Friedman and Simpson, we look at certain mathematical theorems taken from mathematical practice. It turns out that quite a lot of theorems are proof-theoretically equivalent to just five dis- tinguishable subsystems of analysis. The results of this programme are summa- rized in Simpson’s monograph [Sim99]. The five systems considered in reverse mathematics are RCA0, WKL0, ACA0, ATR0 and (Π1-CA)0. All these theories are second order theories and again, the index 0 indicates that induction is restricted to sets. For the precise definition of the theories, we refer to [Sim99]. Here we give only the meaning of the acronyms:
• RCA stands for recursive comprehension axiom. Its set existence axioms yield sets A which are recursive in given sets B1, . . . , Bn.
• WKL stands for weak K¨onig’s Lemma. WKL0 theory extends RCA0 by a formalization of weak K¨onig’s Lemma, expressing that every infinite binary tree has an infinite path.
• ACA stands for arithmetical comprehension axiom. ACA0 can be regarded as the second order analog of Peano arithmetic. In fact, ACA0 is a conser- vative extension of PA.
• ATR stands for arithmetical transfinite recursion. Informally, it expresses that the jump operation can be iterated along any countable well-ordering.
1.5.3 Theories of inductive definition and fixed point theories
Inductive definition is one of the most important concepts in mathematics. Therefore, it is natural to investigate theories which formalize this principle directly. Starting from the theory ID1 of non-iterated induction definitions, iteration yields a natural family of formal systems which are useful for proof theoretic investigation. The theory ID1, one of the most prominent theories in proof theory, may be regarded as the most elementary impredicative theory. Going back to Kreisel [Kre63], its proof-theoretic study (and the study of its iterations) may be found in [Fef70, BFPS81, Poh89].
By dropping the leastness condition for inductive definitions, we get fixed point theories which are of interest in the area of proof-theoretical weak systems. The theory ID1. The theory of non-iterated inductive definitions, ID1, extends Peano arithmetic by postulating the existence of least fixed points for