Local reflection, definable elements and 1-provability

TL;DR

This paper explores local reflection principles, definable elements, and 1-provability, providing new model-theoretic and proof-theoretic insights into their relationships and strength within formal systems.

Contribution

It introduces uniform reflection with definable parameters, relates it to local reflection principles, and offers new proofs and axiomatizations for related logical systems.

Findings

Established the $oldsymbol{oldsymbol{oldsymbol{oldsymbol{ ext{Σ}}_{n+2}}}}$-conservativity of uniform $oldsymbol{oldsymbol{ ext{Σ}}_{n+1}}$-reflection.

Provided a new model-theoretic proof of conservativity results.

Connected 1-provability in $S$ with uniform $oldsymbol{ ext{Σ}}_2$-reflection schema and axiomatized $ ext{I}oldsymbol{ ext{Σ}}_1$.

Abstract

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 $\Sigma_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 $\Sigma_{n+2}$-conservativity of uniform $\Sigma_{n+1}$-reflection over relativized local $\Sigma_{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 $\Sigma_2$-reflection schema and, in particular, obtain an alternative axiomatization of $\mathsf{I}\Sigma_1$.

Equations

$$T⊢\phi ⟹\mathbb{N}\models \phi ,$$

$$\phi (0)\wedge \forall x\left(\phi (x)\to \phi (x+1)\right)\to \forall x\phi (x),\phi (x)\in \Gamma$$

$$\forall x<z\exists y\phi (x,y,a)\to \exists u\forall x<z\exists y<u\phi (x,y,a),\phi (x,y,a)\in {\Sigma }_n.$$

$$\mathsf{EA}⊢\forall x_1,\dots ,x_m\left(\sigma (x_1,\dots ,x_m)\to {\square }_T┌\sigma ({\underline{x}}_1,\dots ,{\underline{x}}_m)┐\right),$$

$${\square }_T\phi \to \phi ,$$

$$\forall x_1,\dots ,x_n\left({\square }_T\phi ({\underline{x}}_1,\dots ,{\underline{x}}_n)\to \phi (x_1,\dots ,x_n)\right),$$

$$\forall x_1,\dots ,x_n{\square }_T\phi ({\underline{x}}_1,\dots ,{\underline{x}}_n)\to {◊}_T\forall x_1,\dots ,x_n\phi (x_1,\dots ,x_n),$$

$$\mathsf{EA}⊢\forall x,y{\square }_T\left({\mathsf{Prf}}_T(\underline{y},┌\phi (\underline{x})┐)\to \phi (\underline{x})\right).$$

$$\forall x{\square }_T\phi (\underline{x})\to \forall x\phi (x),$$

$$\sigma \wedge \forall x{\square }_T(\sigma \to \phi (\underline{x}))\to {◊}_T(\sigma \wedge \forall x\phi (x)),$$

$$\mathsf{EA}⊢\forall x_1,\dots ,x_m(\phi (x_1,\dots ,x_m)\leftrightarrow {\mathsf{True}}_{{\Pi }_n}(┌\phi ({\underline{x}}_1,\dots ,{\underline{x}}_m)┐)),$$

$$\mathsf{EA}⊢\forall \pi \in {\Pi }_n{\square }_T\left(\pi \leftrightarrow {\mathsf{True}}_{{\Pi }_n}(\pi )\right).$$

$$[n{]}_T\phi :=\exists \pi \left({\mathsf{True}}_{{\Pi }_n}(\pi )\wedge {\square }_T(\pi \to \phi )\right),$$

$$\forall x\left(\phi (x)\wedge \forall y\left(\phi (y)\to y=x\right)\to {◊}_T\left[\phi (\underline{x})\wedge \forall y\left(\phi (y)\to y=\underline{x}\right)\right]\right),$$

$$\mathsf{PA}+\mathsf{DRfn}(T)⊢\exists x\neg \phi (x)$$

$$\to \exists x{◊}_T\left(\delta (\underline{x})\wedge \forall y(\delta (y)\to y=\underline{x})\right)$$

$$\to \exists x{◊}_T\neg \phi (\underline{x}),$$

$$\mathsf{PA}+\mathsf{DRfn}(T)⊢\forall x{\square }_T\phi (\underline{x})\to \forall x\phi (x),$$

$$\forall x\left({\square }_T\phi (\underline{x})\to \phi (x)\right),$$

$$\forall x\left({\mathsf{Def}}_{\delta }(x)\to \left({\square }_T\phi (\underline{x})\to \phi (x)\right)\right),$$

$${\mathsf{Def}}_{\delta }(x):=\delta (x)\wedge \forall y,z(\delta (y)\wedge \delta (z)\to y=z)$$

$$\mathsf{EA}+{\mathsf{Rfn}}_{{\Sigma }_k}^n(T)⊢{\mathsf{Def}}_{\delta }(x)\wedge {\square }_T\phi (\underline{x})$$

$$\to [n{]}_T(\delta (\underline{x})\wedge \phi (\underline{x}))$$

$$\to [n{]}_T\exists u(\delta (u)\wedge \phi (u))$$

$$\to \exists u(\delta (u)\wedge \phi (u)).$$

$$\mathsf{EA}+{\mathsf{Rfn}}_{{\Sigma }_k}^n(T)⊢{\mathsf{Def}}_{\delta }(x)\wedge \delta (u)\wedge \phi (u)$$

$$\to \phi (x),$$

$$\mathsf{EA}+{\mathsf{Rfn}}_{{\Sigma }_k}^n(T)⊢{\mathsf{Def}}_{\delta }(x)\to \left({\square }_T\phi (\underline{x})\to \phi (x)\right),$$

$$N\models \sigma (a_1,\dots ,a_m)⟺M\models \sigma (a_1,\dots ,a_m).$$

$$K^{n+1}(M)\models {\mathsf{True}}_{{\Pi }_n}(\pi )\wedge {\square }_T(\pi \to \sigma ).$$

$$M\models {\mathsf{True}}_{{\Pi }_n}(\pi )\wedge {\square }_T({\mathsf{True}}_{{\Pi }_n}(\pi )\to \sigma ),$$

$$M\models {\mathsf{Def}}_{\delta }(\pi )\wedge {\square }_T({\mathsf{True}}_{{\Pi }_n}(\pi )\to \sigma ).$$

$$M\models {\mathsf{True}}_{{\Pi }_n}(\pi )\to \sigma ,$$

Full text

Keywords: reflection principles, 1-provability, definable elements, $\omega$-consistency.

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 $\omega$-consistency. However, in the contemporary formulations of Gödel’s incompleteness theorems a weaker condition of $\Sigma_{1}$-soundness is often used instead of $\omega$-consistency.

On the syntactic level, various semantic notions of soundness are usually translated into the so-called reflection principles. These principles typically express the following form of soundness

[TABLE]

with different conditions being imposed on the formula $\varphi$ and on the notion of provability in $T$. Generalizing Gödel’s consistency assertion $\mathsf{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 G. Kreisel and A. Lévy [11], which allow to conclude that one formal theory $T$ cannot be axiomatized over another formal theory $U$ by the 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 C. Smoryński [15] and L. Beklemishev [4].

Various kinds of reflection principles and consistency assertions for $\mathsf{PA}$ were studied by R. Kaye and H. Kotlarski in [8] from the point of view of ACT-extensions of models (extensions constructed by the means of the arithmetized completeness theorem). More specifically, the authors characterize these principles as the first-order theories of the class of models of $\mathsf{PA}$ having ACT-extensions with certain model-theoretic properties.

One of the principles considered in [8] was the principle of definable reflection $\mathsf{DRfn}(\mathsf{PA})$, which is the restriction of $\mathsf{RFN}(\mathsf{PA})$ to formulas asserting definability of an element, i.e., formulas of the form $\varphi(x)\land\forall y\left(\varphi(y)\rightarrow y=x\right)$. This principle, however, turns out to be equivalent to $\mathsf{RFN}(\mathsf{PA})$.

The idea of considering intermediate principles between local (only standard parameters) and uniform (no restriction on parameters) schemata by allowing restricted use of parameters provides a way to devise new schemata or at least give alternative, sometimes more useful, characterization of the existing principles. In this respect, let us mention the work of A. Cordón-Franco, A. Fernández-Margarit and F. F. Lara-Martín [5], where this idea is applied to the induction schemata. It is shown that parameter-free induction schema is equivalent to its variants with parameters restricted to the certain types of definable elements (cf. Proposition 3.6).

Continuing this line of research, we introduce a refined version of the definable reflection principle, namely, the schema of uniform reflection with $\Sigma_{n}$-definable parameters and show it to be equivalent to the corresponding form of relativized local reflection. This fact is then used to give a rather short model-theoretic proof of the $\Sigma_{n+2}$-conservativity of uniform $\Sigma_{n+1}$-reflection over relativized local $\Sigma_{n+1}$-reflection (Theorem 1). We also establish the connection between this version of reflection principles and the induction schemata with definable parameters introduced in [5] (Corollary 3.7).

Let us also mention the following questions regarding the relationship between local $\omega$-consistency $\omega\textsf{-}\mathsf{Con}(\mathsf{PA})$ and local reflection $\mathsf{Rfn}(\mathsf{PA})$, which were listed as open in [8].

Problem 8.1. Do there exists models $M\models\mathsf{PA}+\mathsf{Rfn}(\mathsf{PA})+\neg\omega\textsf{-}\mathsf{Con}(\mathsf{PA})$?

Problem 8.3. Is it true that $\mathsf{PA}+\mathsf{Rfn}(\mathsf{PA})\not\vdash\omega\textsf{-}\mathsf{Con}^{\mathsf{Th}}(\mathsf{PA})$?

Problem 8.4. Over $\mathsf{PA}$, does $\omega\textsf{-}\mathsf{Con}(\mathsf{PA})$ imply $\mathsf{Con}(\mathsf{PA}+\mathsf{Rfn}(\mathsf{PA}))$?

For the formal definitions of the $\omega$-consistency and reflection principles mentioned in these questions see Section 2.

We show that all of these three questions have positive answer for a wide class of theories $T$ and give a quick solution based on Smoryński’s characterization of the schema $\omega\textsf{-}\mathsf{Con}(T)$ and its restricted variants in terms of partial reflection principles for $T$ (see Theorem 2). Let us note that for the case of $\mathsf{PA}$ these problems have already been solved by V. Yu. Shavrukov (unpublished), see Remark in Section 4 for a further discussion. We also prove the schema $\omega\textsf{-}\mathsf{Con}^{\mathsf{Th}}(T)$ to be equivalent to $\mathsf{RFN}(T)$ (Theorem 4).

Furthermore, we study the assertion (so-called Feferman’s theorem [6, Theorem 4.5]) of $1$-provability in $S$ of the local reflection schema $\mathsf{Rfn}(S)$ and its generalized versions. We relate this assertion to the usual forms of reflection (Theorem 6), which, in particular, allows to give an alternative axiomatization of the theory $\mathsf{I}\Sigma_{1}$ (Corollary 4.6).

The paper is organized as follows. Section 2 introduces the basic notions and notation used throughout this note. In Section 3 we introduce and study the schema of uniform reflection with $\Sigma_{n}$-definable parameters. In Section 4 we give a quick solution to the problems listed above and discuss the proof-theoretic strength of Feferman’s theorem.

2 Preliminaries

In this note we consider first-order theories in the language of arithmetic. As our basic theory we take Elementary arithmetic $\mathsf{EA}$ (sometimes denoted as $\mathsf{I}\Delta_{0}(\exp)$), that is, the first-order theory formulated in the language $0,(\cdot)^{\prime},+,\times$ extended by the unary function symbol $\exp$ for the exponentiation function $2^{x}$. It has the standard defining axioms for these symbols and the induction schema for all elementary formulas (we also call such formulas bounded), i.e., formulas in the language with exponent containing only bounded (by the terms in the language with exponent) quantifiers. The theory $\mathsf{EA}^{+}$ is defined to be an extension of $\mathsf{EA}$ with the axiom asserting the totality of the superexponential function $2^{x}_{y}$.

We define classes $\Sigma_{0}$ and $\Pi_{0}$ to be the classes of all elementary (bounded) formulas. After that the classes $\Sigma_{n}$ and $\Pi_{n}$ of arithmetical hierarchy are defined in a standard way for all $n\geqslant 0$.

If we allow induction for all arithmetical formulas, the resulting theory is Peano arithmetic denoted by $\mathsf{PA}$. For a fixed class of arithmetical formulas $\Gamma$ the fragment of $\mathsf{PA}$ obtained by restricting the induction schema

[TABLE]

to $\Gamma$-formulas without parameters is denoted by $\mathsf{I}\Gamma^{-}$ and called parameter free $\Gamma$-induction. If, in the schema above $\varphi(x)$, is allowed to contain parameters, then we obtain the usual $\Gamma$-induction schema and the corresponding theory is denoted by $\mathsf{I}\Gamma$. We also consider the schema $\mathsf{B}\Sigma_{n}$ of $\Sigma_{n}$-collection

[TABLE]

For more details on these theories, see [9].

All the theories considered in this note are supposed to be recursively axiomatizable consistent extensions of $\mathsf{EA}$. We assume that some standard arithmetization of syntax and the gödelnumbering of syntactic objects has been fixed. In particular, we write $\ulcorner\varphi\urcorner$ for the (numeral of the) gödelnumber of $\varphi$. As usual, each theory $T$ is given to us by an elementary formula $\sigma_{T}(x)$, defining the set of axioms of $T$ in the standard model of arithmetic. The formula $\sigma_{T}(x)$ is used in the construction of the formula $\mathsf{Prf}_{T}(y,x)$ representing the relation “$y$ codes a $T$-proof of the formula with gödelnumber $x$”. The standard provability predicate for $T$ is given by $\exists y\,\mathsf{Prf}_{T}(y,x)$, and we denote this formula by $\Box_{T}(x)$. We often write $\Box_{T}\varphi$ instead of $\Box_{T}(\ulcorner\varphi\urcorner)$ and use the notation $\Diamond_{T}\varphi$ for $\neg\Box_{T}\neg\varphi$ . The sentence $\Diamond_{T}\top$ is the consistency assertion for $T$ and is also denoted by $\mathsf{Con}(T)$.

The predicate $\Box_{T}$ satisfies Löb’s derivability conditions provably in $\mathsf{EA}$ (cf. [4]):

If $T\vdash\varphi$, then $\mathsf{EA}\vdash\Box_{T}\varphi$. 2. 2.

$\mathsf{EA}\vdash\Box_{T}(\varphi\rightarrow\psi)\rightarrow(\Box_{T}\varphi\rightarrow\Box_{T}\psi)$. 3. 3.

$\mathsf{EA}\vdash\Box_{T}\varphi\rightarrow\Box_{T}\Box_{T}\varphi$.

Point 3 follows from the general fact known as provable $\Sigma_{1}$-completeness:

[TABLE]

whenever $\sigma(x_{1},\dots,x_{m})$ is a $\Sigma_{1}$-formula. Here the underline notation $\ulcorner\varphi(\underline{x})\urcorner$ stands for the elementarily definable term, representing the elementary function that maps $k$ to the gödelnumber of the formula $\ulcorner\varphi(\underline{k})\urcorner$. In what follows we usually write just $\Box_{T}\varphi(\underline{x})$ instead of $\Box_{T}\ulcorner\varphi(\underline{x})\urcorner$.

If two theories $T$ and $U$ have the same theorems, we say that they are deductively equivalent and denote this by $T\equiv U$. If they prove the same arithmetical sentences of complexity $\Gamma$, we write $T\equiv_{\Gamma}U$.

In this note we are mainly interested in the following three principles (or schemata) for a given arithmetical theory $T$:

• •

local reflection $\mathsf{Rfn}(T)$:

[TABLE]

for each arithmetical sentence $\varphi$;

• •

uniform reflection $\mathsf{RFN}(T)$:

[TABLE]

for each arithmetical formula $\varphi(x_{1},\dots,x_{n})$;

• •

local $\omega$-consistency $\omega\textsf{-}\mathsf{Con}(T)$:

[TABLE]

for each arithmetical formula $\varphi(x_{1},\dots,x_{n})$.

For a more detailed analysis of the principles above we also consider their partial variants, which are obtained by imposing the restriction $\varphi\in\Gamma$, where $\Gamma$ is some class of arithmetical formulas (usually, $\Sigma_{n}$ or $\Pi_{n}$). Corresponding partial principles are denoted by $\omega\textsf{-}\mathsf{Con}_{\Gamma}(T)$, $\mathsf{Rfn}_{\Gamma}(T)$ and $\mathsf{RFN}_{\Gamma}(T)$, respectively. Partial uniform reflection principles satisfy the equivalence $\mathsf{RFN}_{\Pi_{n+1}}(T)\equiv\mathsf{RFN}_{\Sigma_{n}}(T)$ over $\mathsf{EA}$ for each $n\geqslant 0$ (see [4, Lemma 2.4]).

Note that, in the definitions of $\mathsf{RFN}(T)$ and $\omega\textsf{-}\mathsf{Con}(T)$ (and their partial analogues), by using sequence coding functions, we can, equivalently, restrict these schemata to the formulas $\varphi(x)$ with a single free variable $x$. Let us also mention the following useful principle known as the small reflection (see [4, Lemma 2.2]).

Proposition 2.1**.**

For each formula $\varphi(x)$

[TABLE]

Using this principle one shows that over $\mathsf{EA}$, the schema of uniform reflection $\mathsf{RFN}(T)$ is equivalent to the schema

[TABLE]

for all arithmetical formulas $\varphi(x)$.

In [8] the authors have also considered the following schema $\omega\textsf{-}\mathsf{Con}^{\mathsf{Th}}(T)$ (note that we use slightly different notation), which is a strengthening of $\omega\textsf{-}\mathsf{Con}(T)$,

• •

local $\omega$-consistency of the theory of the model $\omega\textsf{-}\mathsf{Con}^{\mathsf{Th}}(T)$:

[TABLE]

for each arithmetical formula $\varphi(x)$ with a single free variable $x$ and arithmetical sentence $\sigma$.

It is shown that $\omega\textsf{-}\mathsf{Con}^{\mathsf{Th}}(\mathsf{PA})$ implies $\mathsf{Rfn}(\mathsf{PA})$ (take $\varphi(x)$ to be $x=x$) and is implied by $\mathsf{RFN}(\mathsf{PA})$.

It is known that for each $n>0$ there exists an arithmetical $\Pi_{n}$-formula $\mathsf{True}_{\Pi_{n}}(x)$ (known as a truth definition for $\Pi_{n}$-formulas) such that

[TABLE]

for every $\Pi_{n}$-formula $\varphi(x_{1},\dots,x_{m})$, and this fact itself is formalizable in $\mathsf{EA}$, so

[TABLE]

Using these properties, it is not hard to check that over $\mathsf{EA}$, the schema $\mathsf{RFN}_{\Sigma_{n}}(T)$ is equivalent to its universal instance with $\varphi(x)$ taken to be $\neg\mathsf{True}_{\Pi_{n}}(x)$.

The truth predicates are used to define the so-called strong provability predicates. Namely, the following formula

[TABLE]

defines the predicate of $n$-provability, i.e., usual provability in $T$ together with all true $\Pi_{n}$-sentences taken as additional axioms. The predicate $[n]_{T}$ satisfies the same derivability conditions as $\Box_{T}$ and is provably $\Sigma_{n+1}$-complete (see [4]). It is easy to see that $\mathsf{RFN}_{\Sigma_{n+1}}(T)$ is equivalent to $\neg[n]_{T}\bot$ over $\mathsf{EA}$.

The relativized local reflection principles $\mathsf{Rfn}^{n}_{\Gamma}(T)$ are defined analogously to $\mathsf{Rfn}_{\Gamma}(T)$ but with $n$-provability predicate $[n]_{T}$ instead of the usual provability $\Box_{T}$.

3 Reflection with definable parameters

In [8] the authors have introduced the following reflection schema (we formulate it in a dual form, which is actually used in the proofs there), which can be seen as an intermediate scheme between local $\mathsf{Rfn}(T)$ and uniform reflection $\mathsf{RFN}(T)$,

• •

definable reflection $\mathsf{DRfn}(T)$

[TABLE]

for each arithmetical formula $\varphi(x)$ with a single free variable $x$.

It was shown that $\mathsf{DRfn}(\mathsf{PA})$ is actually equivalent to $\mathsf{RFN}(\mathsf{PA})$ using indicators. Let us include a proof of this fact without using indicators.

Proposition 3.1**.**

Over $\mathsf{PA}$, $\mathsf{DRfn}(T)\equiv\mathsf{RFN}(T)$.

Proof.

Clearly, $\mathsf{EA}+\mathsf{RFN}(T)\vdash\mathsf{DRfn}(T)$. To prove the converse fix a formula $\varphi(x)$, and let $\delta(x)$ be the formula $\neg\varphi(x)\land\forall z<x\,\varphi(z)$. We have

[TABLE]

where the first implication uses induction and the second one uses $\mathsf{DRfn}(T)$. By contraposition we obtain

[TABLE]

that is, $\mathsf{PA}+\mathsf{DRfn}(T)\vdash\mathsf{RFN}(T)$. ∎

In this section we consider a refined version of the definable reflection principle, namely, uniform reflection with $\Sigma_{n}$-definable parameters, and use it to give a model-theoretic proof of the $\Sigma_{n+2}$-conservativity of uniform reflection over relativized local reflection (Theorem 1). We also discuss a relationship between these principles and the schemata of induction with definable parameters introduced by A. Cordón-Franco et al. in [5].

Recall the uniform $\Sigma_{k}$-reflection principle $\mathsf{RFN}_{\Sigma_{k}}(T)$:

[TABLE]

where $\varphi(x)$ is a $\Sigma_{k}$-formula. If we require the variable $x$ above to range only over the standard elements (numerals), then we get the schema that is equivalent to local reflection $\mathsf{Rfn}_{\Sigma_{k}}(T)$. We investigate the question: can we expand the range of $x$ to some nonstandard elements while still obtaining the equivalent schema?

Formally, we define the following schema of

• •

uniform $\Sigma_{k}$-reflection with $\Sigma_{n}$-definable parameters $\mathsf{RFN}^{K^{n}}_{\Sigma_{k}}(T)$:

[TABLE]

for each $\Sigma_{n}$-formula $\delta(x)$ and $\Sigma_{k}$-formula $\varphi(x)$, where

[TABLE]

is the formula asserting that $x$ is the unique element satisfying $\delta(x)$.

We aim at proving that these reflection principles are equivalent to their local counterparts.

Proposition 3.2**.**

For each $k>n\geqslant 0$ we have $\mathsf{EA}+\mathsf{Rfn}^{n}_{\Sigma_{k}}(T)\vdash\mathsf{RFN}^{K^{n+1}}_{\Sigma_{k}}(T)$.

Proof.

Fix some $\Sigma_{n+1}$-formula $\delta(x)$ and $\Sigma_{k}$-formula $\varphi(x)$. We will derive the corresponding axiom of $\mathsf{RFN}^{K^{n+1}}_{\Sigma_{k}}(T)$. Using provable $\Sigma_{n+1}$-completeness and an instance of $\mathsf{Rfn}^{n}_{\Sigma_{k}}(T)$ for the $\Sigma_{k}$-sentence $\exists u\,(\delta(u)\land\varphi(u))$ (we use $n<k$ here) we derive

[TABLE]

Since $\mathsf{EA}\vdash\mathsf{Def}_{\delta}(x)\land\delta(u)\rightarrow x=u$, we get

[TABLE]

whence $\mathsf{EA}+\mathsf{Rfn}^{n}_{\Sigma_{k}}(T)\vdash\left(\mathsf{Def}_{\delta}(x)\land\exists u\,(\delta(u)\land\varphi(u))\right)\rightarrow\varphi(x)$, and so

[TABLE]

as required. ∎

In particular, the local $\Sigma_{k}$-reflection is equivalent to the uniform $\Sigma_{k}$-reflection with $\Sigma_{1}$-definable parameters.

Corollary 3.3**.**

For each $k>0$ over $\mathsf{EA}$, $\mathsf{Rfn}_{\Sigma_{k}}(T)\equiv\mathsf{RFN}^{K^{1}}_{\Sigma_{k}}(T)$.

Proof.

By Proposition 3.2 it suffices to show that $\mathsf{EA}+\mathsf{RFN}^{K^{1}}_{\Sigma_{k}}(T)\vdash\Box_{T}\varphi\rightarrow\varphi$, where $\varphi$ is a $\Sigma_{k}$-sentence. Define $\delta(x)$ to be the formula $(x=\underline{0})$ and consider the corresponding axiom of $\mathsf{RFN}^{K^{1}}_{\Sigma_{k}}(T)$. Note that $\mathsf{EA}\vdash\mathsf{Def}_{\delta}(\underline{0})$, whence, by instantiating the axiom with $\underline{0}$, we obtain $\Box_{T}\varphi\rightarrow\varphi$. ∎

Let us recall several notions related to the models of arithmetic (for more details, see [9]). Given a model $M$ and a natural number $n$ we denote by $K^{n}(M)$ the substructure of $M$ consisting of all $\Sigma_{n}$-definable elements without parameters. Given a substructure $N\subseteq M$, we say that $N$ is a $\Sigma_{n}$-elementary substructure (denoted $N\prec_{\Sigma_{n}}M$) if and only if for each $\Sigma_{n}$-formula $\sigma(x_{1},\dots,x_{m})$ and $a_{1},\dots a_{m}\in N$

[TABLE]

The models $K^{n+1}(M)$ possess the following useful property (see Remark (i) after Theorem 2.1 in [9]).

Lemma 3.4**.**

For each $n\geqslant 0$, $K^{n+1}(M)\prec_{\Sigma_{n+1}}M$, whenever $M\models\mathsf{I}\Sigma^{-}_{n}$.

We have the following generalization of Corollary 3.3.

Proposition 3.5**.**

For each $k>n\geqslant 0$ over $\mathsf{EA}+\mathsf{I}\Sigma^{-}_{n}$, $\mathsf{Rfn}^{n}_{\Sigma_{k}}(T)\equiv\mathsf{RFN}^{K^{n+1}}_{\Sigma_{k}}(T)$.

Proof.

By Proposition 3.2 $\mathsf{EA}+\mathsf{Rfn}^{n}_{\Sigma_{k}}(T)\vdash\mathsf{RFN}^{K^{n+1}}_{\Sigma_{k}}(T)$, so we only prove the converse implication (over $\mathsf{EA}+\mathsf{I}\Sigma^{-}_{n}$). Fix some $\Sigma_{k}$-sentence $\sigma$ and a model $M$ of $\mathsf{EA}+\mathsf{I}\Sigma^{-}_{n}+\mathsf{RFN}^{K^{n+1}}_{\Sigma_{k}}(T)$. We will show that $M\models[n]_{T}\sigma\rightarrow\sigma$, whence the result follows, so assume $M\models[n]_{T}\sigma$. By Lemma 3.4 we have $K^{n+1}(M)\prec_{\Sigma_{n+1}}M$, implying $K^{n+1}(M)\models[n]_{T}\sigma$, since $[n]_{T}\sigma$ is a $\Sigma_{n+1}$-sentence. It follows that there exists a $\pi\in K^{n+1}(M)$ such that

[TABLE]

Using $K^{n+1}(M)\prec_{\Sigma_{n+1}}M$ again, we get $M\models\mathsf{True}_{\Pi_{n}}(\pi)\land\Box_{T}(\pi\rightarrow\sigma)$, whence

[TABLE]

since $\mathsf{EA}\vdash\forall\pi\in\Pi_{n}\,\Box_{T}\left(\pi\leftrightarrow\mathsf{True}_{\Pi_{n}}(\pi)\right)$ and $M\models\mathsf{EA}$. Let $\delta(x)$ be a $\Sigma_{n+1}$-formula such that $M\models\mathsf{Def}_{\delta}(\pi)$. We have

[TABLE]

Now, since $\mathsf{True}_{\Pi_{n}}(\pi)\rightarrow\sigma$ is a $\Sigma_{k}$-formula, we can use $\mathsf{RFN}^{K^{n+1}}_{\Sigma_{k}}(T)$ in $M$ to obtain

[TABLE]

whence $M\models\sigma$, as required, since $M\models\mathsf{True}_{\Pi_{n}}(\pi)$ by (1). ∎

Now we can give a relatively short model-theoretic proof of the following consequence of the so-called reduction property (see [3, Proposition 4.6]).

Theorem 1**.**

If $U$ is a $\Pi_{n+2}$-axiomatized extension of $\mathsf{EA}$, then

[TABLE]

Proof.

The inclusion $\supseteq$ is clear from the definitions of the schemata and $[n]_{T}$, so we only prove the converse. Assume $U+\mathsf{RFN}_{\Sigma_{n+1}}(T)\vdash\sigma$, where $\sigma$ is a $\Sigma_{n+2}$-sentence. Fix an arbitrary model $M\models U+\mathsf{Rfn}^{n}_{\Sigma_{n+1}}(T)$. We will show that $M\models\sigma$. By point (i) of Theorem 1 from [2], $\mathsf{EA}+\mathsf{Rfn}^{n}_{\Sigma_{n+1}}(\mathsf{EA})\vdash\mathsf{I}\Sigma^{-}_{n}$, whence, certainly, $U+\mathsf{Rfn}^{n}_{\Sigma_{n+1}}(T)\vdash\mathsf{I}\Sigma^{-}_{n}$, and so, in particular, $M\models\mathsf{EA}+\mathsf{I}\Sigma^{-}_{n}$. Lemma 3.4 then implies $K^{n+1}(M)\prec_{\Sigma_{n+1}}M$.

We have $K^{n+1}(M)\models U$, since $M\models U$ and $U$ is a $\Pi_{n+2}$-extension (the truth of $\Pi_{n+2}$-sentences is preserved downwards by the relation $\prec_{\Sigma_{n+1}}$). We will show that $K^{n+1}(M)\models\mathsf{RFN}_{\Sigma_{n+1}}(T)$. In this case $K^{n+1}(M)\models U+\mathsf{RFN}_{\Sigma_{n+1}}(T)$, whence, by the assumption, $K^{n+1}(M)\models\sigma$, so $M\models\sigma$, as required, since $\sigma$ is a $\Sigma_{n+2}$-sentence (the truth of $\Sigma_{n+2}$-sentences is preserved upwards by the relation $\prec_{\Sigma_{n+1}}$).

The rest of the proof is close to that of Proposition 3.5. Aiming for a contradiction, assume $K^{n+1}(M)\not\models\mathsf{RFN}_{\Sigma_{n+1}}(T)$, i.e., there exists a $\Sigma_{n+1}$-formula $\varphi(x)$ and an element $a\in K^{n+1}(M)$ with $K^{n+1}(M)\models\Box_{T}\varphi(\underline{a})\land\neg\varphi(a),$ which, using $K^{n+1}(M)\prec_{\Sigma_{n+1}}M$, implies

[TABLE]

Let $\delta(x)$ be a $\Sigma_{n+1}$-formula such that $M\models\mathsf{Def}_{\delta}(a)$. Since $M\models\mathsf{EA}+\mathsf{Rfn}^{n}_{\Sigma_{n+1}}(T)$, Proposition 3.2 implies that $M\models\mathsf{RFN}^{K^{n+1}}_{\Sigma_{n+1}}(T)$ and, in particular,

[TABLE]

since $\varphi(x)$ is a $\Sigma_{n+1}$-formula. Together with (2) this yields $M\models\varphi(a)$, which contradicts $M\models\neg\varphi(a)$ in (2). ∎

Let us also note the following relationship between Proposition 3.5 and the following proposition proved in [5, Proposition 4.1] (we use slightly different notation).

Proposition 3.6**.**

For each $n\geqslant 0$ over $\mathsf{EA}+\mathsf{I}\Sigma^{-}_{n}$,

[TABLE]

Here $\mathsf{I}(\Sigma^{-}_{n+1},K^{n+1})$ is the local variant of $\Sigma_{n+1}$-induction schema, where the conclusion of the induction axiom is relativized to $\Sigma_{n+1}$-definable elements (for the formal definitions of this schema and $\mathsf{I}(\Sigma_{n+1},I^{n+1},K^{n+1}_{1})$, see [5]). Thus, Proposition 3.5 can be seen as an analogue of Proposition 3.6 but for the reflection principles instead of the induction schemata.

The connection between the two propositions is based on the following fact (see [2, Theorem 1 (ii)] for $n>0$ and [5, Theorem 5.2] for $n=0$), for each $n\geqslant 0$

[TABLE]

In view of this result, Propositions 3.5 and 3.6 we have the following

Corollary 3.7**.**

For each $n\geqslant 0$ over $\mathsf{EA}+\mathsf{I}\Sigma^{-}_{n}$,

[TABLE]

This may be contrasted with the famous result by D. Leivant [12] and H. Ono [13] (cf. [4, Theorem 7]), that $\mathsf{EA}+\mathsf{RFN}_{\Sigma_{n+2}}(\mathsf{EA})\equiv\mathsf{I}\Sigma_{n+1}$ for each $n\geqslant 0$, and a result by L. Beklemishev (see [2, Theorem 1 (i)]), that $\mathsf{EA}+\mathsf{Rfn}^{n+1}_{\Sigma_{n+2}}(\mathsf{EA})\equiv\mathsf{I}\Sigma^{-}_{n+1}$ for each $n\geqslant 0$. In our case we also have the equivalence between certain forms of $\Sigma_{n+2}$-reflection for $\mathsf{EA}$ and $\Sigma_{n+1}$-induction, namely, for the versions of reflection and induction restricted to $\Sigma_{n+1}$-definable elements.

4 Local reflection, $\omega$-consistency and 1-provability

In this section we show how Smoryński’s characterization of the local $\omega$-consistency assertions in terms of reflection principles can be used to give a quick solution to the problems from [8] mentioned in the introduction. We also prove that the schema $\omega\textsf{-}\mathsf{Con}^{\mathsf{Th}}(T)$, introduced in [8], is actually equivalent to $\mathsf{RFN}(T)$ (Theorem 4). In addition, we study the proof-theoretic strength of Feferman’s theorem and its generalized versions (Theorem 6). In particular, we obtain an alternative characterization of $\mathsf{I}\Sigma_{1}$ in terms of Feferman’s theorem for $\mathsf{EA}$ (Corollary 4.6).

The following characterization of the local $\omega$-consistency schemata in terms of reflection principles was obtained by C. Smoryński (see [14, Theorem 1.1.c]).

Theorem 2**.**

Over $\mathsf{EA}$,

1. (i)

$\omega\textsf{-}\mathsf{Con}_{\Sigma_{n}}(T)\equiv\mathsf{Rfn}_{\Sigma_{2}}(T+\mathsf{RFN}_{\Sigma_{n}}(T))$* for each $n>0$,* 2. (ii)

$\omega\textsf{-}\mathsf{Con}_{\Sigma_{0}}(T)\equiv\mathsf{Rfn}_{\Sigma_{1}}(T)$.

The following theorem, which solves Problem 8.4, is a consequence of Theorem 2.

Theorem 3**.**

$\mathsf{EA}+\omega\textsf{-}\mathsf{Con}_{\Sigma_{1}}(T)\vdash\mathsf{Con}(T+\mathsf{Rfn}(T)).$**

Proof.

Point (i) of Theorem 2 implies that $\mathsf{EA}+\omega\textsf{-}\mathsf{Con}_{\Sigma_{1}}(T)\vdash\mathsf{Con}(T+\mathsf{RFN}_{\Sigma_{1}}(T))$, whence the result follows, once we show that

[TABLE]

We clearly have $\mathsf{EA}\vdash\mathsf{Con}(T+\mathsf{RFN}_{\Sigma_{1}}(T))\rightarrow\mathsf{Con}(T+\mathsf{Rfn}_{\Sigma_{1}}(T))$. Also the following $\Pi_{1}$-conservativity result is provable in $\mathsf{EA}$ (see [3, Proposition 5.1.(ii)]),

[TABLE]

As a consequence, these two theories are provably equiconsistent

[TABLE]

whence (3) follows immediately.

∎

In particular, $\mathsf{PA}+\omega\textsf{-}\mathsf{Con}_{\Sigma_{1}}(\mathsf{PA})\vdash\mathsf{Con}(\mathsf{PA}+\mathsf{Rfn}(\mathsf{PA}))$, which solves Problem 8.4 and, consequently, Problems 8.1 and 8.3 as well, because then

[TABLE]

by Gödel’s second incompleteness theorem, whence, certainly,

[TABLE]

Recall from Section 2 that $\omega\textsf{-}\mathsf{Con}^{\mathsf{Th}}(\mathsf{PA})$ is implied by $\mathsf{RFN}(\mathsf{PA})$. We prove that these two schemata are equivalent for an arbitrary theory $T$, which provides an alternative solution to Problem 8.3.

Theorem 4**.**

Over $\mathsf{EA}$, $\omega\textsf{-}\mathsf{Con}^{\mathsf{Th}}(T)\equiv\mathsf{RFN}(T)$.

Proof.

To derive $\omega\textsf{-}\mathsf{Con}^{\mathsf{Th}}(T)$ from $\mathsf{RFN}(T)$ argue as follows

[TABLE]

where the first and the last implications use $\mathsf{RFN}(T)$.

To show the converse fix a formula $\varphi(x)$ with a single free variable $x$. We show

[TABLE]

whence $\mathsf{EA}+\omega\textsf{-}\mathsf{Con}^{\mathsf{Th}}(T)\vdash\mathsf{RFN}(T)$ follows. Denote the sentence $\neg\forall x\,\varphi(x)$ by $\sigma$ and argue by contraposition

[TABLE]

which yields (4).

∎

In particular, $\mathsf{PA}+\mathsf{Rfn}(\mathsf{PA})\not\vdash\omega\textsf{-}\mathsf{Con}^{\mathsf{Th}}(\mathsf{PA})$, since $\mathsf{PA}+\mathsf{Rfn}(\mathsf{PA})\not\vdash\mathsf{RFN}(\mathsf{PA})$, which gives another solution to Problem 8.3.

In order to formulate these corollaries of Theorem 2 for an arbitrary theory $T$ in place of $\mathsf{PA}$ we recall the following definition. A theory $T$ is said to have infinite characteristic, if the theory $T_{\omega}$ is consistent, where

[TABLE]

It is known that the theory $T+\mathsf{Rfn}(T)$ is equiconsistent with $T_{\omega}$ (see [4, Corollary 2.35]) . This fact together with Theorem 3 and Gödel’s second incompleteness theorem yields the following

Corollary 4.1**.**

For each theory $T$ of infinite characteristic

[TABLE]

Remark. The author learned (personal communication) that the mentioned problems were already solved by V. Shavrukov back in 2010 (unpublished). His proof, which he kindly provided to us, also uses Smoryński’s characterization of $\omega\textsf{-}\mathsf{Con}(T)$ and is almost identical to ours except one minor point. Let us present his proof and make some comments concerning its relationship to our proof. It goes as follows

[TABLE]

which again solves Problem 8.4 and the other two problems as well. The second implication in the above proof uses the following fact [14, Theorem 5.1.i],

[TABLE]

While this is true for the theories containing $\mathsf{I}\Sigma_{1}$, it does not hold for weaker theories, e.g., $\mathsf{EA}$ or $\mathsf{EA}^{+}$.

Let us comment on this issue a little bit more. It is well-known (the so-called Feferman theorem [6, Theorem 4.5]) that the local reflection schema $\mathsf{Rfn}(S)$ for a consitent r.e. theory $S$ is contained in $S$ together with the set $\mathsf{Th}_{\Pi_{1}}(\mathbb{N})$ of all true $\Pi_{1}$-sentences.

The usual informal proof goes as follows. For a given instance $\Box_{S}\psi\rightarrow\psi$ of $\mathsf{Rfn}(S)$ consider two possibilities: either $S\vdash\psi$ or $S\not\vdash\psi$. In the first case we have $S\vdash\Box_{S}\psi\rightarrow\psi$, and in the second case, since $\neg\Box_{S}\psi$ is a true $\Pi_{1}$-sentence, we obtain $S+\mathsf{Th}_{\Pi_{1}}(\mathbb{N})\vdash\neg\Box_{S}\psi$, implying $S+\mathsf{Th}_{\Pi_{1}}(\mathbb{N})\vdash\Box_{S}\psi\rightarrow\psi$.

It follows that each theorem of the theory $S+\mathsf{Rfn}(S)$ is provable in $S+\mathsf{Th}_{\Pi_{1}}(\mathbb{N})$. Natural formalization of the above proof gives

[TABLE]

However, the formalization of 1-provability in $S$ of each theorem of $S+\mathsf{Rfn}(S)$, i.e., the following $\Pi_{3}$-sentence

[TABLE]

cannot be proven in $\mathsf{EA}$ (and even in $\mathsf{EA}^{+}$).

To derive (6) in $\mathsf{I}\Sigma_{1}$ from 1-provability of each axiom (5), one can use $\Sigma_{2}$-collection schema $\mathsf{B}\Sigma_{2}$ (since the provability predicate $[1]_{S}$ is $\Sigma_{2}$) in the same way as $\mathsf{B}\Sigma_{1}$ is usually applied to conclude the provability of each theorem given that of each axiom for $\Sigma_{1}$-provability predicates (see, e.g., [3, Proposition 5.1] for this type of argument). After that $\Pi_{3}$-conservativity of $\mathsf{B}\Sigma_{2}$ over $\mathsf{I}\Sigma_{1}$ (see [1, Theorem 4.1]) yields the provability of (6) in $\mathsf{I}\Sigma_{1}$ (cf. Theorem 6 below for $T=\mathsf{EA}$). As for the non-provability of (6) in $\mathsf{EA}^{+}$, we have the following

Proposition 4.2**.**

$\mathsf{EA}^{+}\not\vdash\forall\varphi\left(\Box_{S+\mathsf{Rfn}(S)}\varphi\rightarrow[1]_{S}\varphi\right)$.

Proof.

Aiming at a contradiction assume $\mathsf{EA}^{+}$ proves (6). Instantiating $\varphi$ with $\bot$, we get that $\mathsf{Con}(S+\mathsf{Rfn}(S))$ is provable in $\mathsf{EA}^{+}+\neg[1]_{S}\bot$, i.e., in $\mathsf{EA}+\mathsf{RFN}_{\Sigma_{1}}(S)$, since $\mathsf{EA}^{+}$ is contained in the latter theory. But $\mathsf{EA}+\mathsf{RFN}_{\Sigma_{1}}(S)$ is $\Sigma_{2}$-conservative over $\mathsf{EA}+\mathsf{Rfn}_{\Sigma_{1}}(S)$ (see [3, Proposition 4.6]), whence

[TABLE]

contradicting Gödel’s second incompleteness theorem. ∎

A natural question to ask then is whether the formalized version of Feferman’s result (6) is actually equivalent to $\mathsf{I}\Sigma_{1}$ over a weaker theory? We establish this equivalence and, in fact, we obtain a more general result using $\mathsf{EA}^{+}$-provable characterization of the set $C_{S}(T)=\{\varphi\mid T\vdash[1]_{S}\varphi\}$ in terms of iterated local reflection principles for $S$.

See [10] for the precise definitions of iterated local reflection principles $\mathsf{Rfn}(S)_{\alpha}$ and the corresponding notion of $\Sigma^{0}_{2}$-ordinal $|T|_{\Sigma^{0}_{2}}$ of a theory. The following theorem, which is a formalization of the equivalence $C_{S}(T)\equiv\mathsf{Rfn}(S)_{1+\alpha}$ for “nice” ($\mathsf{EA}^{+}$-provably $\Sigma^{0}_{2}$-regular) theories $T$, was obtained in [10, Theorem 5.3].

Theorem 5**.**

For each $\mathsf{EA}^{+}$-provably $\Sigma^{0}_{2}$-regular theory $T$ with $\Sigma^{0}_{2}$-ordinal $\alpha$

[TABLE]

Natural examples of such theories $T$ and corresponding $\Sigma^{0}_{2}$-ordinals $|T|_{\Sigma^{0}_{2}}$ are listed in the table below. Here $\omega_{0}:=1$, $\omega_{n+1}:=\omega^{\omega_{n}}$ and $\varepsilon_{0}=\sup\{\omega_{n}\mid n<\omega\}$. See [10] for more examples and details.

[TABLE]

Let us denote by $\mathsf{RFN}_{[1]_{S}}(T)$ the uniform $T$-reflection schema for $[1]_{S}$-formulas, i.e., the following $\Pi_{3}$-sentence

[TABLE]

Theorem 5 immediately yields the following

Corollary 4.3**.**

For each $\mathsf{EA}^{+}$-provably $\Sigma^{0}_{2}$-regular theory $T$ with $\Sigma^{0}_{2}$-ordinal $\alpha$, the following are equivalent over $\mathsf{EA}^{+}$

• (i)

$\mathsf{RFN}_{[1]_{S}}(T)$,

• (ii)

$\forall\varphi\left(\Box_{\mathsf{Rfn}(S)_{1+\alpha}}\varphi\rightarrow[1]_{S}\varphi\right)$.

Now, we need to relate $\mathsf{RFN}_{[1]_{S}}(T)$ with the schema $\mathsf{RFN}_{\Sigma_{2}}(T)$. This is done by applying the generalized version of the Friedman-Goldfarb-Harrington principle (see [7] for various generalizations of this principle). Note the presence of $\mathsf{B}\Sigma_{1}$ in our formulation, since our formalization of 1-provability predicate $[1]_{S}$ is slightly different from that of [7].

Lemma 4.4**.**

For each $\Sigma_{2}$-formula $\sigma(x)$ there is a formula $\varphi(x)$ such that

• (i)

$\mathsf{EA}\vdash\sigma(x)\lor[1]_{S}\bot\rightarrow[1]_{S}\varphi(\underline{x})$,

• (ii)

$\mathsf{EA}+\mathsf{B}\Sigma_{1}\vdash[1]_{S}\varphi(\underline{x})\rightarrow\sigma(x)\lor[1]_{S}\bot$.

Proof.

Let $\sigma(x)$ be $\exists y\,\psi(y,x)$ for $\Pi_{1}$-formula $\psi(y,x)$, and let $\chi(z,\theta)$ be the formula $\exists\pi<z\left(\mathsf{True}_{\Pi_{1}}(\pi)\land\mathsf{Prf}_{S}(z,\ulcorner\pi\rightarrow\theta\urcorner)\right)$. We clearly have $\mathsf{EA}\vdash[1]_{S}\theta\leftrightarrow\exists z\,\chi(z,\theta).$ Consider the following fixed-point

[TABLE]

To prove $(i)$ note that, clearly, $[1]_{S}\bot$ implies $[1]_{S}\varphi(\underline{x})$, so we only show

[TABLE]

Fix $y$ such that $\psi(y,x)$ and argue under $[1]_{S}$. The proof of $\varphi(\underline{x})$ goes by considering two cases. If the second member of the conjunction in the definition of $\varphi(x)$ is true, i.e., $\forall z<\underline{y}\,\neg\chi(z,\ulcorner\varphi(\underline{x})\urcorner)$, then, since we also have $\psi(\underline{y},\underline{x})$, being a true $\Pi_{1}$-sentence, we obtain $\varphi(\underline{x})$. Otherwise, $\exists z\leqslant\underline{y}\,\chi(z,\ulcorner\varphi(\underline{x})\urcorner)$. This formula is equivalent to the disjunction, since $\underline{y}$ is a numeral, so it is sufficient to prove the following

[TABLE]

The proof of the above goes by induction on $y$, which is formalizable in $\mathsf{EA}$, since we can bound the code of the corresponding $S$-proof by some elementary term $p(y)$. The induction step goes through, once the following fact is established

[TABLE]

This follows from the small reflection principle (see Proposition 2.1). Indeed, argue under $\Box_{S}$ and assume $\chi(\underline{z},\ulcorner\varphi(\underline{x})\urcorner)$, that is, $\exists\pi<\underline{z}\left(\mathsf{True}_{\Pi_{1}}(\pi)\land\mathsf{Prf}_{S}(\underline{z},\ulcorner\pi\rightarrow\varphi(\underline{x})\urcorner)\right)$. Again, this $\Pi_{1}$-sentence $\pi$ is standard, so $\mathsf{True}_{\Pi_{1}}(\pi)$ is equivalent to $\pi$ (and the proof of this fact is bounded by the fixed elementary term of $z$ and, consequently, of $y$), since we have

[TABLE]

The small reflection principle yields $\pi\rightarrow\varphi(\underline{x})$ from $\mathsf{Prf}_{S}(\underline{z},\ulcorner\pi\rightarrow\varphi(\underline{x})\urcorner)$, whence $\varphi(\underline{x})$ follows.

To prove $(ii)$ assume $[1]_{S}\varphi(\underline{x})$ and $\neg\sigma(x)$. We prove $[1]_{S}\neg\varphi(\underline{x})$, whence $[1]_{S}\bot$ follows. Recall that

[TABLE]

Denote the formula in the brackets by $\theta(y,x)$. Fix $u$ such that $\chi(u,\ulcorner\varphi(\underline{x})\urcorner)$ (follows from $[1]_{S}\varphi(\underline{x})$) and argue under $[1]_{S}$. To prove $\neg\varphi(\underline{x})$, i.e., $\forall y\,\theta(y,\underline{x})$, we fix an arbitrary $y$ and consider two cases. If $\underline{u}\leqslant y$, then since we have $\chi(\underline{u},\ulcorner\varphi(\underline{x})\urcorner)$ under $[1]_{S}$, being a true $\Sigma_{2}$-sentence, we obtain $\exists z\leqslant y\,\chi(z,\ulcorner\varphi(\underline{x})\urcorner)$, where we can take $z$ to be $\underline{u}$, which itself implies $\theta(y,\underline{x})$. If we have $y<\underline{u}$, then it is left to prove the following ($u$ can be treated as a free variable)

[TABLE]

since the formula under $[1]_{S}$ implies $\theta(y,\underline{x})$. Again, since $\underline{u}$ is standard, it is sufficient to prove

[TABLE]

By provable $\Sigma_{1}$-completeness we have

[TABLE]

so we need to prove

[TABLE]

This is where $\Sigma_{1}$-collection schema $\mathsf{B}\Sigma_{1}$ is used. Applying $\Sigma_{1}$-collection to the formula $\forall y<u\,\Box_{S}\neg\psi(\underline{y},\underline{x})$, we get a sequence of $S$-proofs $\psi(\underline{y},\underline{x})$ for $y<u$, and then we concatenate them (and make some other trivial transformations) to obtain the proof of $\bigwedge_{y<u}\neg\psi(\underline{y},\underline{x})$.

Combining the above proofs of $\theta(y,\underline{x})$ under $[1]_{S}$ for the two cases considered above, we obtain

[TABLE]

which proves $(ii)$. ∎

The next lemma shows that $\mathsf{RFN}_{[1]_{S}}(T)$ is equivalent to the full $\Sigma_{2}$-reflection schema $\mathsf{RFN}_{\Sigma_{2}}(T)$ over $\mathsf{EA}+\mathsf{B}\Sigma_{1}+\neg[1]_{S}\bot$.

Lemma 4.5**.**

• (i)

$\mathsf{EA}\vdash\mathsf{RFN}_{\Sigma_{2}}(T)\rightarrow\mathsf{RFN}_{[1]_{S}}(T)$,

• (ii)

$\mathsf{EA}+\mathsf{B}\Sigma_{1}+\neg[1]_{S}\bot\vdash\mathsf{RFN}_{[1]_{S}}(T)\rightarrow\mathsf{RFN}_{\Sigma_{2}}(T)$.

Proof.

Point $(i)$ is clear, since $[1]_{S}\varphi$ is a $\Sigma_{2}$-formula.

The reverse implication $(ii)$ follows from Lemma 4.4. Fix $\varphi(x)$ obtained by applying this lemma to $\Sigma_{2}$-formula $\sigma(x)$. We then have

[TABLE]

i.e., $\mathsf{EA}+\mathsf{B}\Sigma_{1}+\neg[1]_{S}\bot\vdash\mathsf{RFN}_{[1]_{S}}(T)\rightarrow\mathsf{RFN}_{\Sigma_{2}}(T)$, as required. ∎

The following theorem, which is a direct corollary of Lemma 4.5 and Corollary 4.3, demonstrates that over a weaker theory, $\mathsf{RFN}_{\Sigma_{2}}(T)$ is equivalent to the generalized Feferman theorem.

Theorem 6**.**

For each $\mathsf{EA}^{+}$-provably $\Sigma^{0}_{2}$-regular theory $T$ with $\Sigma^{0}_{2}$-ordinal $\alpha$

• (i)

$\mathsf{EA}+\mathsf{RFN}_{\Sigma_{2}}(T)\vdash\forall\varphi\left(\Box_{\mathsf{Rfn}(S)_{1+\alpha}}\varphi\rightarrow[1]_{S}\varphi\right)$,

• (ii)

$\mathsf{EA}+\mathsf{B}\Sigma_{1}+\neg[1]_{S}\bot+\forall\varphi\left(\Box_{\mathsf{Rfn}(S)_{1+\alpha}}\varphi\rightarrow[1]_{S}\varphi\right)\vdash\mathsf{RFN}_{\Sigma_{2}}(T)$.

In particular, taking $T$ and $S$ to be $\mathsf{EA}$ we obtain the following alternative axiomatization of the theory $\mathsf{I}\Sigma_{1}$.

Corollary 4.6**.**

The following theories are deductively equivalent

• (i)

$\mathsf{I}\Sigma_{1}$,

• (ii)

$\mathsf{EA}+\mathsf{RFN}_{\Sigma_{2}}(\mathsf{EA})$,

• (iii)

$\mathsf{EA}^{+}+\mathsf{B}\Sigma_{1}+\forall\varphi\left(\Box_{\mathsf{EA}+\mathsf{Rfn}(\mathsf{EA})}\varphi\rightarrow[1]_{\mathsf{EA}}\varphi\right)$.

Proof.

The equivalence $(i)\Leftrightarrow(ii)$ is well-known (cf. [4, Theorem 7]). The equivalence $(ii)\Leftrightarrow(iii)$ follows from the previous corollary, since $\mathsf{I}\Sigma_{1}$ contains $\mathsf{EA}^{+}+\mathsf{B}\Sigma_{1}$ and $\mathsf{EA}+\neg[1]_{\mathsf{EA}}\bot\equiv\mathsf{EA}^{+}$. ∎

Acknowledgements

The author would like to thank Lev D. Beklemishev for useful discussions and his comments on the draft of the paper. The author would also like to thank Vladimir Yu. Shavrukov for informing us about his solution of the mentioned problems and presenting his proof to us, which lead to the investigation of the formalizability of Feferman’s theorem.

The reported study was funded by RFBR, project number 19-31-90050.