Local reflection, definable elements and 1-provability
- PDF / 351,406 Bytes
- 18 Pages / 439.37 x 666.142 pts Page_size
- 16 Downloads / 178 Views
Mathematical Logic
Local reflection, definable elements and 1-provability Evgeny Kolmakov1,2 Received: 15 July 2019 / Accepted: 18 March 2020 © Springer-Verlag GmbH Germany, part of Springer Nature 2020
Abstract In this note we study several topics related to the schema of local reflection Rfn(T ) and its partial and relativized variants. Firstly, we introduce the principle of uniform reflection with Σn -definable parameters, establish its relationship with relativized local reflection principles and corresponding versions of induction with definable parameters. Using this schema we give a new model-theoretic proof of the Σn+2 conservativity of uniform Σn+1 -reflection over relativized local Σn+1 -reflection. We also study the proof-theoretic strength of Feferman’s theorem, i.e., the assertion of 1-provability in S of the local reflection schema Rfn(S), and its generalized versions. We relate this assertion to the uniform Σ2 -reflection schema and, in particular, obtain an alternative axiomatization of IΣ1 . Keywords Reflection principles · Definable elements · Peano arithmetic · 1-provability Mathematics Subject Classification 03F30
1 Introduction In the original formulation of Gödel’s first incompleteness theorem no semantic concepts, such as soundness, were used. Instead, Gödel used a rather strong syntactic notion of ω-consistency. However, in the contemporary formulations of Gödel’s incompleteness theorems a weaker condition of Σ1 -soundness is often used instead of ω-consistency.
The reported study was funded by RFBR, project number 19-31-90050.
B
Evgeny Kolmakov [email protected]
1
Lomonosov Moscow State University, Moscow, Russia
2
Steklov Mathematical Institute of Russian Academy of Sciences, Moscow, Russia
123
E. Kolmakov
On the syntactic level, various semantic notions of soundness are usually translated into so-called reflection principles. These principles typically express the following form of soundness T ϕ
⇒
N | ϕ,
with different conditions being imposed on the formula ϕ and on the notion of provability in T . Generalizing Gödel’s consistency assertion Con(T ), principles of this kind provide plenty of true sentences which are nevertheless unprovable in T . Reflection principles were shown to be a convenient tool for the analysis of formal theories by demonstrating that many other principles, e.g., induction or different forms of consistency, can be expressed as some form of reflection and due to the unboundedness theorems of Kreisel and Lévy [11], which allow to conclude that one formal theory T cannot be axiomatized over another formal theory U by arithmetical sentences of a certain logical complexity, whenever T proves the corresponding form of reflection for U . For a survey of the results on reflection principles, see Smory´nski [15] and Beklemishev [4]. Various kinds of reflection principles and consistency assertions for PA were studied by Kaye and Kotlarski in [8] from the point of view of ACT-extensions of models (extensions constructed by the means of the arithmet
Data Loading...
