Iterated local reflection versus iterated consistency
type: Item
instance of: scholarly article
title: Iterated local reflection versus iterated consistency
zbMATH Open document ID: 0848.03031
DOI: 10.1016/0168-0072(95)00007-4
published in: Annals of Pure and Applied Logic
publication date: 1996-10-27T00:00:00Z
review text: If you add the sentence `\(T\) is consistent' to a theory \(T\) (large enough), you get a theory \(T'\) larger than \(T\). Repeating this transfinitely often you produce a transfinite progression \((T_\alpha)\), basing on iteration of consistency. If \(\alpha\) is chosen from a recursive notation system, this progression is called recursive. If the same procedure is performed using the so-called local reflection principle instead of consistency, another progression \((T^\alpha)\) is gained. In this case every step consists of adding the formulas \(\text{Pr}_T (\ulcorner A \urcorner) \to A\) as axioms to \(T\) for every sentence \(A\) of the language of \(T\), \(\text{Pr}_T\) being the provability predicate for \(T\). Starting from \textit{A. Turing}'s fundamental work [Proc. Lond. Math. Soc., II. Ser. 45, 161-228 (1939; Zbl 0021.09704)], \textit{S. Feferman} considered such progressions in J. Symb. Log. 27, 259-316 (1963; Zbl 0117.25402). Already Turing stated and Feferman pointed out precisely that the ordinals used cannot be taken from an arbitrary stock. The progressions depend on the chosen recursive description of the underlying well-ordering. Moreover the numeration of the axioms of the theories affects the progression. Connections between the different kinds of iterations can be found in papers of \textit{G. Kreisel} and \textit{A. Lévy} [Z. Math. Logik Grundlagen Math. 14, 97-142 (1968; Zbl 0167.01302)], \textit{S. N. Artemov} [Vopr. Kibern., Mosk. 75, 3-22 (1982; Zbl 0499.03046)], and \textit{S. V. Goryachev} [Mat. Zametki 40, No. 5, 561-571 (1986; Zbl 0632.03044)]. In the present paper the following precise relations are proven to hold under certain conditions: \[ (T^\alpha)_\beta \equiv_{\Pi^0_1} T_{\omega^\alpha (1 + \beta)}, \quad (T^\beta)_\alpha \equiv_{\Pi^0_1} T_{\beta + \omega^\alpha} \tag{*} \] where \(\equiv_{\Pi^0_1}\) means that in both theories the same \(\Pi^0_1\)-formulas are provable. To express the restrictions on (*), the author defines t…
Mathematics Subject Classification ID: 03F35
Mathematics Subject Classification ID: 03F15
zbMATH DE Number: 802545
zbMATH Keywords: iterated reflection
zbMATH Keywords: iterated consistency
zbMATH Keywords: PRA
zbMATH Keywords: transfinite progression
zbMATH Keywords: provability
zbMATH Keywords: nice well-orderings
zbMATH Keywords: smooth numerations
author: Lev D. Beklemishev
reviewed by: Helmut Pfeiffer
MaRDI profile type: Publication
full work available at URL: 0168-0072(95)00007-4
OpenAlex ID: W1974965205
cites work: Q3218104
cites work: Q3964565
cites work: Provability logics for natural Turing progressions of arithmetical theories
cites work: On bimodal logics of provability
cites work: Reflection principles and iterated consistency assertions
cites work: Transfinite recursive progressions of axiomatic theories
cites work: Reflection Principles and their Use for Establishing the Complexity of Axiomatic Systems
cites work: Solution of a problem of Leon Henkin
cites work: Q3325707
cites work: Q4749830
cites work: Q3866106
cites work: Fragments of arithmetic
cites work: Q3140643
cites work: Systems of Logic Based on Ordinals†
cites work: The formalization of interpretability
Recommended article: Proof Theoretic Analysis by Iterated Reflection
Recommended article: Reflection algebras and conservation results for theories of iterated truth
Recommended article: Autonomous progression and transfinite iteration of self-applicable truth
Recommended article: Proof-theoretic analysis by iterated reflection
Recommended article: Consistency proof via pointwise induction
Recommended article: The logic of Turing progressions
Recommended article: Q4348126
Recommended article: Q4215632
Recommended article: How to characterize provably total functions by local predicativity
Recommended article: Variation on a theme of Schütte
description: scientific article; zbMATH DE number 802545