×

Reflection schemes and provability algebras in formal arithmetic. (English. Russian original) Zbl 1097.03054

Russ. Math. Surv. 60, No. 2, 197-268 (2005); translation from Usp. Mat. Nauk 60, No. 2, 3-78 (2005).
This paper is a rather complete survey of proof-theoretic results (and methods) based on reflections principles in arithmetic. From the Introduction (p. 200):
In §1 we introduce basic concepts concerning formal arithmetic. We also consider basic properties of the provability formula and give short proofs of theorems due to Gödel, Rosser, and Löb.
In §2 we study general properties of local and uniform reflection principles and prove the so-called Kreisel-Lévy unboundedness theorems.
In §3 we present basic facts concerning provably total computable functions of theories and their relations to reflection principles.
In §4 we establish results relating induction and reflection schemata in arithmetic. We show that the natural fragments of PA defined by various restrictions of the induction schema correspond precisely (are deductively equivalent) to certain reflection schemata over elementary arithmetic EA. We also prove here a conservation result for uniform reflection schemata over reflection rules, the so-called reduction property, which plays an important role below.
Together with the results of §2, this enables us to obtain answers to a number of questions concerning various properties of fragments of PA by using a unified method. […]
In §5 we study the notion of provability algebra and use it as a basis for our approach to the ordinal analysis of Peano arithmetic. We give a new consistency proof of PA by transfinite induction up to the ordinal \(\varepsilon_0\). We also give a simple example of a true combinatorial statement motivated by provability algebras that is unprovable in Peano arithmetic. Finally, we establish a relationship between provability algebras and Turing-Feferman transfinite progressions of iterated reflection principles. Using this relationship, we obtain a characterization of \(\Pi_n\)-consequences of PA in terms of such progressions and draw some other interesting corollaries.

MSC:

03F45 Provability logics and related algebras (e.g., diagonalizable algebras)
03F15 Recursive ordinals and ordinal notations
03F30 First-order arithmetic and fragments
03F05 Cut-elimination and normal-form theorems
03F40 Gödel numberings and issues of incompleteness
03-02 Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations
PDFBibTeX XMLCite
Full Text: DOI