Evgeny Kolmakov | Searcharxiv

arXiv2019

Local reflection, definable elements and 1-provability

In this note we study several topics related to the schema of local reflection $\mathsf{Rfn}(T)$ and its partial and relativized variants. Firstly, we introduce the principle of uniform reflection with $Σ_n$-definable parameters, establish its relationship with the 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 $\mathsf{Rfn}(S)$, and its generalized versions. We relate this assertion to the uniform $Σ_2$-reflection schema and, in particular, obtain an alternative axiomatization of $\mathsf{I}Σ_1$.

math.LO↗

arXiv2018

Axiomatizing provable $n$-provability

A formula $ϕ$ is called \emph{$n$-provable} in a formal arithmetical theory $S$ if $ϕ$ is provable in $S$ together with all true arithmetical $Π_{n}$-sentences taken as additional axioms. While in general the set of all $n$-provable formulas, for a fixed $n>0$, is not recursively enumerable, the set of formulas $ϕ$ whose $n$-provability is provable in a given r.e.\ metatheory $T$ is r.e. This set is deductively closed and will be, in general, an extension of $S$. We prove that these theories can be naturally axiomatized in terms of progressions of iterated local reflection principles. In particular, the set of provably 1-provable sentences of Peano arithmetic PA can be axiomatized by $\varepsilon_0$ times iterated local reflection schema over PA. Our characterizations yield additional information on the proof-theoretic strength of these theories (w.r.t. various measures of it) and on their axiomatizability. We also study the question of speed-up of proofs and show that in some cases a proof of $n$-provability of a sentence can be much shorter than its proof from iterated reflection principles.

math.LO↗