1 Introduction
The following benchmark results showcase the relationship between uniform reflection and induction in the context of first order arithmetic:
$$ \begin{align} \mathsf{EA}+ \mathrm{RFN}(\mathsf{EA})\ =\ \mathsf{PA}, \end{align} $$
where
$\mathsf {EA}$
is Kalmár elementary arithmetic, and
$$ \begin{align} \mathsf{PA}+\mathrm{RFN}(\mathsf{PA}) \ =\ \mathsf{PA}+\mathrm{TI}(\varepsilon_0). \end{align} $$
Equation (1) is usually attributed to [Reference Kreisel and Lévy12]. Equation (2) is a special case of [Reference Kreisel and Lévy12, Theorem 12].
This note is concerned with uniform reflection in the context of second order arithmetic.Footnote 1 It can be gleaned from Kreisel and Lévy [Reference Kreisel and Lévy12, Theorem 14] that
$$\begin{align*}\mathsf{RCA} +\mathrm{RFN}(\mathsf{RCA}) \ = \ \mathsf{RCA} +\mathrm{TI}(\varepsilon_0), \end{align*}$$
where
$\mathsf {RCA}$
is
$\mathsf {RCA}_0$
together with full induction.Footnote
2
The same proof-theoretic methods of [Reference Kreisel and Lévy12], namely, formalized cut elimination, show that Equations (1) and (2) lift up to any theory T of second order arithmetic of the form
$T_0$
together with full induction, where
$T_0$
is any finitely axiomatizable extension of
$\mathsf {RCA}_0$
. We thus have (see Theorem 3.1)
$$ \begin{align} T_0 + \mathrm{RFN}(T_0) \ = \ T, \end{align} $$
$$ \begin{align} T_0 + \mathrm{RFN}(T) \ = \ T_0 + \mathrm{TI}(\varepsilon_0). \end{align} $$
More in general (cf. [Reference Kreisel and Lévy12, Theorem 12]),
$$\begin{align*}T_0+ \mathrm{RFN}(T+\mathrm{TI}(\alpha)) \ =\ T_0 + \mathrm{TI}(\varepsilon(\alpha)), \end{align*}$$
where
$\varepsilon (\alpha )$
is the least
$\varepsilon $
-number beyond
$\alpha $
. The schema
$\mathrm {TI}(\alpha )$
of transfinite induction along
$\alpha $
consists of formulas
$$\begin{align*}\forall x\, (\forall y\prec x\, \varphi(y)\rightarrow \varphi(x))\rightarrow \forall x\, \varphi(x), \end{align*}$$
where
$\varphi (x)$
ranges over all formulas and
$\prec $
is a primitive recursive ordinal notation system for
$\alpha $
.
Anyone familiar with (a bit of) ordinal analysis will readily realize that (3) and (4) hold because of the unlimited amount of induction, respectively transfinite induction up to
$\varepsilon _0$
, available. The point we are trying to make is that the so-called
$\varPi ^1_1$
proof-theoretic ordinals of
$T_0$
and T may be way bigger than
$\varepsilon _0$
. Recall that the
$\varPi ^1_1$
proof-theoretic ordinal
$|S|$
of a second order arithmetic theory S can be defined as the supremum of the provably well-founded ordinals of S. These are the ordinals
$\alpha $
such that
$S\vdash \mathrm {WF}(\alpha )$
, where
$\mathrm {WF}(\alpha )$
expresses the well-foundedness of
$\alpha $
and corresponds to the following single instance of transfinite induction:
$$\begin{align*}\forall X\, (\forall \beta\, (\forall \gamma<\beta\, (\gamma\in X) \rightarrow \beta\in X)\rightarrow \forall \beta<\alpha \, (\beta\in X)). \end{align*}$$
Actually, one always works with a given primitive recursive ordinal notation system, so that the above definition is relative to the choice of such notation system (see [Reference Rathjen18] for an overview). Now, under certain conditions (cf. [Reference Rathjen18, Proposition 2.13]),
$|S|$
coincides with the least ordinal
$\alpha $
such that
$$\begin{align*}S+\mathrm{WF}(\alpha)\vdash \mathrm{Con}(S). \end{align*}$$
Again, the above definition refers to a given ordinal notation system. In particular, for theories of great proof-theoretic strength, it is certainly not the case that
$T_0 + \mathrm {WF}(\varepsilon _0) \vdash \mathrm {Con}(T_0)$
, let alone
$T_0 + \mathrm {WF}(\varepsilon _0) \vdash \mathrm {RFN}(T)$
. So much for that.
A more subtle point is that the restriction to finitely axiomatizable theories is a necessary one, as the result does not apply to recursively enumerable theories
$T_0$
of bounded complexity. The assumption plays a role in the direction from (transfinite) induction to reflection. The reason, roughly speaking, is that an infinite theory may not prove that all its axioms are true. In fact, for sufficiently strong theories, such condition entails finite axiomatizability. Note that main subsystems of reverse mathematics, the so-called Big Five, are finitely axiomatizable [Reference Simpson21]. We refer to Section 4 for a discussion of this issue.
In this note we obtain the following refinement of (3) and (4). We show in Theorem 5.1 that if
$T_0$
is any theory of second order arithmetic extending
$\mathsf {RCA}_0$
and axiomatized by a
$\varPi ^1_2$
(in general,
$\varPi ^1_{k+2}$
) sentence, T is
$T_0$
plus full induction, and
$n\geq 1$
(in general,
$n\geq k+1$
), then over
$T_0$
$$ \begin{align} \mathrm{RFN}_{\varPi^1_{n+2}}(T_0) \ = \ \mathrm{I}{\varPi^1_n} \ \supseteq \ (\mathrm{I}\varPi^1_n)^{-} \ = \ \mathrm{RFN}_{\varSigma^1_{n+1}}(T_0), \end{align} $$
$$ \begin{align} \mathrm{RFN}_{\varPi^1_{n+2}}(T) \ = \ \mathrm{TI}_{\varPi^1_n}(\varepsilon_0) \ \supseteq \ \mathrm{TI}_{\varPi^1_n}(\varepsilon_0)^{-} \ = \ \mathrm{RFN}_{\varSigma^1_{n+1}}(T). \end{align} $$
The superscript
${}^-$
refers to the restriction of the pertaining schema to formulas without set parameters. We prove in Theorem 5.3 that, under certain conditions, the inclusions in (5) and (6) are strict. This is obtained by a standard application of Gödel’s second incompleteness theorem.
In first order arithmetic we have a neat correspondence between uniform reflection and induction (see [Reference Leivant13, Reference Ono15]): for all
$n\geq 1$
,
$$\begin{align*}\mathsf{EA} + \mathrm{RFN}_{\varPi_{n+2}}(\mathsf{EA})\ =\ \mathsf{EA} +\mathrm{RFN}_{\varSigma_{n+1}}(\mathsf{EA})\ =\ \mathsf{EA} + \mathrm{I}{\varPi_n}. \end{align*}$$
If anything, we can say that a less clear-cut picture emerges when we move to second order arithmetic.Footnote
3
On the other hand (cf. [Reference Pakhomov and Walsh17, Section 3.1]), one could recover the equivalence between
$\varPi ^1_{n+2}$
and
$\varSigma ^1_{n+1}$
uniform reflection by considering a relativized version of uniform reflection with set parameters. More precisely, given a set X of natural numbers and a second order arithmetic theory T, let
$T(X)$
be the extension of T with oracle axioms
$\bar n\in \bar X$
for
$n\in X$
and
$\bar n\notin \bar X$
for
$n\notin X$
, where
$\bar X$
is a new set constant. Note that this construction makes sense in
$\mathsf {RCA}_0$
since the theory
$T(X)$
is recursive in T and X. One can then introduce the schema
$\mathrm {RFN}^*(T)$
given by formulas
Now, the proofs of Theorems 3.1 and 5.1 go through mutatis mutandis. Note that
is provable in
$\mathsf {RCA}_0$
. In particular, one obtains
$$ \begin{align*} T_0 + \mathrm{RFN}_{\varPi^1_{n+2}}^*(T_0) &= \ T_0 + \mathrm{I}{\varPi^1_n} \ = \ T_0 + \mathrm{RFN}_{\varSigma^1_{n+1}}^*(T_0), \\ T_0 + \mathrm{RFN}_{\varPi^1_{n+2}}^*(T) & = \ T_0 + \mathrm{TI}_{\varPi^1_n}(\varepsilon_0) \ =\ T_0 + \mathrm{RFN}_{\varSigma^1_{n+1}}^*(T), \end{align*} $$
where
$T_0$
, T, and n are as above.
2 Basics
2.1 First order arithmetic
For the purposes of this paper, let the language of first order arithmetic consist of finitely many symbols including
$0,1,+,\times ,=,<$
. As usual,
$\varDelta _0=\varPi _0=\varSigma _0$
denotes the class of formulas built up from atomic formulas by means of Boolean connectives and bounded quantifiers of the form
$\exists x< t$
and
$\forall x<t$
, where t is a term. The arithmetic hierarchy for
$n>0$
is thus defined:
$\varPi _{n+1}=\{\forall x\, \varphi (x)\mid \varphi (x)\in \varSigma _n\}$
and dually
$\varSigma _{n+1} =\{ \exists x\, \varphi (x)\colon \varphi (x)\in \varPi _n\}$
.
2.2 Reflection
We assume a primitive recursive Gödel numbering
of formulas. The uniform reflection principle
$\mathrm {RFN}(T)$
for a theory T is a schema consisting of formulas
where
$\varphi (x)$
is a formula with at most the displayed free variable and
$\mathrm {Pr}_T(y)$
is a canonical provability predicate for T (cf. [Reference Feferman5, Reference Feferman6]). The formula
can be seen as an abbreviation of
Here,
$\sigma (u,x,y)$
is a
$\varSigma _1$
formula defining the primitive recursive operation
, where v is the only free variable of
$\varphi $
and
$\varphi (\bar n/v)$
denotes the substitution of the numeral
$\bar n$
for v in
$\varphi $
. For ease of notation, we omit the overline notation for numerals when writing
inside a formula.
2.3 Second order arithmetic
The language of second order arithmetic is two-sorted, with first order variables
$x,y,z,\ldots $
intended to range over natural numbers, and second order variables
$X,Y,Z,\ldots $
intended to range over sets of natural numbers. It is obtained from the language of first order arithmetic by adding a membership relation symbol
$\in $
connecting the two sorts. The equality relation symbol
$=$
only applies to first order terms.
The classes of formulas
$\varDelta ^0_0$
,
$\varPi ^0_n$
, and
$\varSigma ^0_n$
are defined just as in the first order case, but now set parameters are allowed. In this context, a formula is arithmetic if it does not contain set quantifiers, that is, quantifications of the form
$\forall X$
and
$\exists X$
. Note that an arithmetic formula may contain free set variables. A formula is
$\varPi ^1_n$
if it is of the form
$\forall X_1\, \exists X_2 \cdots Q X_n\,\varphi $
, where
$\varphi $
is arithmetic. The definition of
$\varSigma ^1_n$
formulas is dual.
The theory known as (full) second order arithmetic, often denoted
$\mathsf {Z}_2$
, is given by the usual first order axioms for zero, successor, addition, multiplication, and less than relation, together with comprehension and induction schemata
$$ \begin{align} \exists X\,\forall x\,(x\in X\leftrightarrow \varphi(x)), \end{align} $$
$$ \begin{align} \varphi(0)\land \forall x\,(\varphi(x)\rightarrow \varphi(x+1))\rightarrow\forall x\, \varphi(x), \end{align} $$
where
$\varphi $
ranges over all formulas. Note that every instance of induction can be obtained from comprehension and the induction axiom
$$\begin{align*}0\in X\land \forall x\,(x\in X\rightarrow x+1\in X)\rightarrow \forall x\,(x\in X). \end{align*}$$
The main subsystems of reverse mathematics [Reference Simpson21], also known as the Big Five, are obtained by prescribing how much induction one can use and what sets one can form (in terms of comprehension or set existence axioms). These are
$\mathsf {RCA}_0$
(Recursive Comprehension Axiom),
$\mathsf {WKL}_0$
(Weak König’s Lemma),
$\mathsf {ACA}_0$
(Arithmetical Comprehension Axiom),
$\mathsf {ATR}_0$
(Arithmetical Transfinite Recursion), and
$\varPi ^1_1$
-
$\mathsf {CA}_0$
(Comprehension for
$\varPi ^1_1$
formulas).
$\mathsf {RCA}_0$
, the standard base theory of reverse mathematics, consists of
$\varDelta ^0_1$
comprehension and
$\varSigma ^0_1$
induction. It is well known that
$\mathsf {RCA}_0$
is a conservative extension of
$\mathrm {I}\varSigma _1$
, that is, Peano arithmetic
$\mathsf {PA}$
with induction restricted to
$\varSigma _1$
formulas. The theory
$\mathsf {ACA}_0$
consists of comprehension and induction for all arithmetic formulas.
2.4 Partial truth definitions
In first order arithmetic one has access for any
$n\geq 1$
to a
$\varSigma _n$
(resp.
$\varPi _n$
) partial truth definition for the class
$\varSigma _n$
(resp.
$\varPi _n$
) over
$\mathrm {I}\varSigma _1$
. The construction involves a partial truth definition for
$\varDelta _0$
formulas, of complexity
$\varDelta _1$
over
$\mathrm {I}\varSigma _1$
(cf. [Reference Hájek and Pudlák9, Chapter 1, Section 1(d)]). By the same token, one can construct partial truth definitions for formulas of bounded complexity, say of bounded rank, over
$\mathrm {I}\varSigma _1$
(cf. [Reference Troelstra22, Chapter 1, Section 5.4]).
In the context of second order arithmetic, one can define truth predicates for arithmetic formulas and
$\varPi ^1_n$
formulas but they fail to be provably so over weak fragments such as
$\mathsf {RCA}_0$
. However, for the purposes of this paper, it will be sufficient to work with partial truth definitions for formulas of bounded complexity. Let
$R_m$
denote the class of formulas of rank at most m and let
$P_{n,m}$
denote the (closure under subformulas of the) class of
$\varPi ^1_n$
formulas with arithmetic matrix of rank at most m. We define the rank as usual: the rank is a natural number and the rank of a compound formula is bigger than the rank of its components. Notice that we make no distinction between number and set quantifiers. The construction of partial truth definitions in first order arithmetic easily extends to arithmetic formulas with set parameters. In particular, for any choice of n and m, one obtains a partial truth predicate for
$R_m$
and a
$\varPi ^1_n$
truth predicate for
$P_{n,m}$
formulas over
$\mathsf {RCA}_0$
.
We will use partial truth definitions of the first kind (for
$R_m$
) in the proof of Theorem 3.1. In Theorem 5.1 we will choose a
$\varPi ^1_n$
partial truth definition for sufficiently many
$\varPi ^1_n$
formulas, namely, for a sufficiently large class of the form
$P_{n,m}$
.
At one point (see Lemma 5.2) we will use the fact that
$\varPi ^1_n$
(resp.
$\varSigma ^1_n$
) uniform reflection can be finitely axiomatized over
$\mathsf {ACA}_0$
for each
$n\geq 1$
. This can be attained by means of universal formulas. We say that a
$\varPi ^1_n$
formula
$\varphi _U(e,x)$
with displayed free variables is universal
$\varPi ^1_n$
in a theory T if for all
$\varPi ^1_n$
formulas
$\varphi (x)$
, T proves
. Universal
$\varSigma ^1_n$
formulas are defined in the exact same way. The existence in
$\mathsf {ACA}_0$
of universal
$\varPi ^1_n$
and
$\varSigma ^1_n$
formulas for every
$n\geq 1$
is basically folklore. There is some leeway in designing universal formulas. For example, one possible route involves the following two steps in the construction of a universal
$\varPi ^1_1$
formula with set parameters; it is then routine to build up universal
$\varPi ^1_n$
and
$\varSigma ^1_n$
formulas for all
$n\geq 1$
. First, given a
$\varSigma ^0_1$
formula
$\varphi (x,f,X_1,\ldots , X_k)$
, where f denotes a function from
$\omega $
to
$\omega $
, one can primitive recursively find an index e such that
$$ \begin{align*} \varphi(x,f,X_1,\ldots,X_k) & \leftrightarrow \{e\}^{f\oplus X_1\oplus\cdots \oplus X_k}(x)\downarrow\, \\ & \leftrightarrow \exists s\, \vartheta(e,x,s,\bar f(s), \bar X_1(s),\ldots,\bar X_k(s)), \end{align*} $$
where
$\vartheta (e,x,s,z)$
is a fixed
$\varDelta ^0_0$
formula,
$\bar f(s)$
encodes the sequence
${\langle f(0),\ldots ,f(s-1)\rangle }$
, and
$\bar X_i(s)$
encodes the first s bits of the characteristic function of
$X_i$
. This version of the enumeration theorem can be formalized in
$\mathsf {RCA}_0$
(cf. [Reference Simpson21, Theorem II.2.7, p. 68]). Second, given a
$\varPi ^1_1$
formula
$\varphi (x,X_1,\ldots ,X_k)$
, one can primitive recursively construct a
$\varSigma ^0_1$
formula
$\varphi _0(x,f,X_1,\ldots ,X_k)$
such that
$\varphi (x,X_1,\ldots ,X_k)\leftrightarrow \forall f\, \varphi _0(x,f,X_1,\ldots ,X_k)$
. This is Kleene normal form theorem for
$\varPi ^1_1$
formulas and can be formalized in
$\mathsf {ACA}_0$
(cf. [Reference Simpson21, Lemma V.1.4, p. 169]). Another approach (cf. [Reference Pakhomov and Walsh16, Section 2.1]) is to further formalize the second step with the help of a partial truth definition for
$\varSigma ^0_1$
formulas.
We refer the reader to [Reference Pakhomov and Walsh16, Section 2.1] for more background on partial truth predicates in second order arithmetic.
3 The uniform reflection principle in analysis
In this section we outline a proof of the following theorem.
Theorem 3.1 [Reference Kreisel and Lévy12].
Let
$T_0\supseteq \mathsf {RCA}_0$
be a finitely axiomatizable second order arithmetic theory. Let T be
$T_0$
plus the schema of full induction. Then
$$ \begin{align} T_0 +\mathrm{RFN}(T_0)= T, \end{align} $$
$$ \begin{align} T_0 + \mathrm{RFN}(T)= T_0 + \mathrm{TI}(\varepsilon_0). \end{align} $$
Proof (3) For the forward direction note that for every standard n the formula
$$\begin{align*}\varphi(0)\land \forall x\,(\varphi(x)\rightarrow \varphi(x+1)) \rightarrow \varphi(\bar n) \end{align*}$$
is provable in classical logic, and hence in any theory whatsoever. The construction of such a proof is primitive recursive (indeed elementary recursive) in n. This can be formalized in
$\mathsf {RCA}_0$
. Therefore
It follows that
$$\begin{align*}T_0 +\mathrm{RFN}(T_0)\vdash \forall x\,(\varphi(0)\land \forall x\,(\varphi(x)\rightarrow \varphi(x+1)) \rightarrow \varphi(x)), \end{align*}$$
which is classically equivalent to induction for
$\varphi $
.
For the other direction, we use cut elimination for classical logic, which is available in
$\mathsf {RCA}_0$
. More in detail, fix a sentence
$\psi $
axiomatizing
$T_0$
and let
$\varphi (x)$
be given. We aim to show
For convenience, let us consider a Tait style sequent calculus for classical logic.Footnote
4
We reason informally in T. If
$\varphi (\bar n)$
is provable in
$T_0$
, then there is a finite cut-free proof of the sequent
$\neg \psi , \varphi (\bar n)$
. By induction on the height of the proof, one shows that every sequent in the proof is true. Now,
$\psi $
is true, and so
$\varphi (\bar n)$
must be true. The induction argument can be formalized in
$\textsf {RCA}$
with the aid of a partial truth predicate for
$R_m$
such that both
$\neg \psi $
and
$\varphi (x)$
are in
$R_m$
. Note in fact that by the subformula property a cut-free proof consists only of subformulas of the end sequent.
(4) The proof that
$T_0 + \mathrm {RFN}(T)$
entails
$\mathrm {TI}(\varepsilon _0)$
is based on a straightforward generalization of Gentzen’s lifting result [Reference Gentzen8, p. 293] (i.e., the closure of provable transfinite induction under
$\alpha \mapsto \omega ^{\alpha }$
over
$\mathsf {PA}$
). Let
$\mathrm {Prog}(\varphi )$
be a shorthand for
$\forall x\,(\forall y\prec x\,\varphi (y)\rightarrow \varphi (x))$
. Then for every formula
$\varphi (x)$
and for every standard number k, T proves
$$\begin{align*}\mathrm{Prog}(\varphi)\rightarrow \forall x\prec \omega_k\, \varphi(x), \end{align*}$$
where
$\omega _0=1$
and
$\omega _{k+1}=\omega ^{\omega _k}$
. The construction of such a proof is uniform and gives a primitive recursive function that accepts a
$\varPi ^1_n$
formula
$\varphi (x)$
and a standard number
$k>0$
as inputs and outputs a proof in
$\mathsf {RCA}_0$
plus induction for
$\varPi ^1_{n+k}$
formulas of
$\mathrm {Prog}(\varphi )\rightarrow \forall x\prec \omega _{k+1}\,\varphi (x)$
. This formalizes in
$\mathsf {RCA}_0$
. The upshot is that
Therefore
$$\begin{align*}T_0 +\mathrm{RFN}(T)\vdash \forall z\,(\mathrm{Prog}(\varphi)\rightarrow \forall x\prec \omega_z\, \varphi(x)). \end{align*}$$
The conclusion follows.
The converse direction (cf. the proof of [Reference Kreisel and Lévy12, Theorem 14]) is based on the fact that in a suitable infinitary system for
$\omega $
-arithmetic one can eliminate cuts and then prove by transfinite induction on
$\varepsilon _0$
that every sequent in a cut-free
$\omega $
-proof is true.
More in detail, let
$\psi $
be a sentence axiomatizing
$T_0$
. Given a formula
$\varphi $
, we aim to show
Again, let us consider a two-sorted extension of a finitary Tait sequent calculus for
$\mathsf {PA}$
, call it
$\mathsf {PA}^2$
, and its infinitary counterpart with the
$\omega $
-rule, call it
$\mathsf {PA}^2_{\infty }$
.Footnote
5
We reason informally in
$T_0 + \mathrm {TI}(\varepsilon _0)$
. If T proves
$\varphi (\bar n)$
, then there is a proof of the sequent
$\neg \psi ,\varphi (\bar n)$
in
$\mathsf {PA}^2$
. We first convert such a finite proof into an
$\omega $
-proof of
$\neg \psi ,\varphi (\bar n)$
in
$\mathsf {PA}^2_{\infty }$
of height
$<\omega \cdot 2$
and cut formulas of rank
$<{\kern-2pt}r$
, for some natural number r.Footnote
6
By applying full cut elimination, we then obtain a cut-free
$\omega $
-proof of height
$<\varepsilon _0$
. We can now show that every sequent in the proof is true by transfinite induction on
$\varepsilon _0$
. As before, since
$\psi $
is true,
$\varphi (\bar n)$
must be true. This concludes the proof.
Let us notice that the embedding of
$\mathsf {PA}$
into an infinitary system with the
$\omega $
-rule, call it
$\mathsf {PA}_{\infty }$
, and cut elimination thereof (see, e.g., [Reference Schütte19, Theorems 22.8 and 28.5]) extends to
$\mathsf {PA}^2$
and
$\mathsf {PA}^2_{\infty }$
in a straightforward manner. On the other hand, it is by now clear how to formalize all this in, e.g.,
$\mathsf {RCA}_0$
by considering
$\omega $
-proofs with ordinal tags below
$\varepsilon _0$
.Footnote
7
In particular,
$\omega $
-proofs can be directly represented as infinite trees (see [Reference Friedman and Sheard7, Reference Mints14]) or suitably coded by numbers (see [Reference Buchholz4, Reference Schwichtenberg20]). What matters is that being (a code of) an
$\omega $
-proof of height less than
$\varepsilon _0$
can be expressed in an arithmetic way, whether this is a property about sets or about numbers (it can be
$\varPi ^0_1$
[Reference Schwichtenberg20] or even primitive recursive [Reference Buchholz4]). We point out that for the purposes of cut elimination a key element of any such coding appears to be Mint’s repetition rule [Reference Mints14]. Finally, the argument by transfinite induction can be formalized by using a partial truth predicate as before, thanks to the fact that cut-free proofs (provably) enjoy the subformula property.
4 Some remarks
The proof of uniform reflection from (transfinite) induction relies on partial truth definitions and the assumption that
$T_0$
is finitely axiomatizable. We have already addressed in Section 2 how to deal with partial truth definitions over
$\mathsf {RCA}_0$
. With regard to finite axiomatizability, it is clear that any sufficiently strong finite theory can prove its own truth. In fact, if
$T_0\supseteq \mathsf {RCA}_0$
is axiomatized by a sentence
$\psi $
, then
$$\begin{align*}T_0\vdash \mathrm{Ax}_{T_0}(x)\rightarrow \mathrm{Tr}(x), \end{align*}$$
by letting
$\mathrm {Ax}_{T_0}(x)$
be
, where
$\mathrm {Tr}(x)$
is a partial truth definition for a sufficiently large class of sentences including
$\psi $
. Conversely, under mild conditions, every theory capable of proving its own truth must be finitely axiomatizable.
Proposition 4.1. Let
$T\supseteq S$
be a recursively enumerable theory and
$S\supseteq \mathsf {RCA}_0$
be finitely axiomatizable. Suppose there is predicate
$\mathrm {T}(x)$
such that
$$\begin{align*}T\vdash \mathrm{Ax}_T(x)\rightarrow \mathrm{T}(x), \end{align*}$$
where
$\mathrm {Ax}_T$
is a
$\varSigma _1$
definition of T, and suppose that
for every axiom
$\varphi \in T$
. Then T is finitely axiomatizable.
Proof The theory
$S +\{\forall x\,(\mathrm {Ax}_T(x)\rightarrow \mathrm {T}(x))\}$
is finitely axiomatizable and equivalent to T. Note that, by
$\varSigma _1$
completeness,
for every
$\varphi \in T$
.
In general, Theorem 3.1 fails for infinite theories of bounded complexity (e.g., axioms with a bound on the number of set quantifiers or even axioms with bounded rank). The following simple example is a case in point.
Example 4.2. Let
$T_0$
be
$\mathsf {RCA}_0 +\{ \emptyset ^{(\bar n)} \text { exists }\colon n\in \omega \}$
. Note that
$\mathsf {RCA}_0$
is finitely axiomatizable and hence
$T_0$
is equivalent to a theory of bounded rank.Footnote
8
We claim that
$T_0 +\mathrm {TI}(\varepsilon _0)$
does not prove uniform reflection over
$T_0$
. In fact,
. By reflection one would obtain
$$\begin{align*}T_0 +\mathrm{TI}(\varepsilon_0)\vdash \forall x\,(\emptyset^{(x)} \text{ exists}). \end{align*}$$
A standard compactness argument shows that there is a model of
$T_0 +\mathrm {TI}(\varepsilon _0)$
where
$\forall x\,(\emptyset ^{(x)} \text { exists})$
fails. In the compactness argument use the fact that for every n the
$\omega $
-model
$\{X\subseteq \omega \colon X\leq _T \emptyset ^{(n)}\}$
is a model of
$\mathsf {RCA}_0 + \mathrm {TI}(\varepsilon _0)$
that satisfies
$$\begin{align*}\emptyset^{(\bar n)} \text{ exists and } \exists x\,(\emptyset^{(x)} \text{ does not exist}). \end{align*}$$
5 Fragments
Let
$\mathrm {RFN}_{\varPi ^1_n}(T)$
be the restriction of
$\mathrm {RFN}(T)$
to
$\varPi ^1_n$
formulas. The schema
$\mathrm {RFN}_{\varSigma ^1_n}(T)$
is defined similarly. Observe that the uniform reflection schema applies to formulas
$\varphi (x)$
with no free variables other than x. Therefore, the schemata
$\mathrm {RFN}_{\varPi ^1_n}(T)$
and
$\mathrm {RFN}_{\varSigma ^1_n}(T)$
refer to
$\varPi ^1_n$
and
$\varSigma ^1_n$
formulas
$\varphi (x)$
with no free variables, in particular no free set variables, other than x. However, we can apply uniform reflection to formulas with finitely many number variables. Note that in first order arithmetic the schema
is equivalent (over
$\mathsf {EA}$
) to the schema with only one variable (see, e.g., [Reference Feferman6]). The same applies to restrictions of uniform reflection in the
$\varPi _n$
and
$\varSigma _n$
hierarchy. Similarly,
$\varPi ^1_n$
uniform reflection is equivalent (over
$\mathsf {RCA}_0$
) to its multivariate version. The same holds for
$\varSigma ^1_n$
uniform reflection. For example, given a
$\varPi ^1_n$
formula
$\varphi (x_1,\ldots ,x_k)$
with the free variables shown, consider the formula
$$\begin{align*}\psi(x)\ =_{\mathrm{def}}\ \forall x_1\cdots\forall x_k\,((x)_1=x_1\land\cdots\land (x)_k=x_k\rightarrow \varphi(x_1,\ldots,x_k)). \end{align*}$$
Then
$\psi (x)$
is
$\varPi ^1_n$
in
$\mathsf {RCA}_0$
,
and
For a fine characterization of uniform reflection, we need to consider lightface versions of induction and transfinite induction up to
$\varepsilon _0$
. Let
$(\mathrm {I}\varPi ^1_n)^{-}$
be the restriction of induction to
$\varPi ^1_n$
formulas with no set parameters. The same definition applies to
$\mathrm {TI}_{\varPi ^1_n}(\varepsilon _0)$
.
Theorem 5.1. Let
$T_0\supseteq \mathsf {RCA}_0$
be a second order arithmetic theory axiomatized by a
$\varPi ^1_2$
sentence, and let
$n\geq 1$
. Let T denote
$T_0$
plus the schema of full induction. Over
$T_0$
,
$$ \begin{align} \mathrm{RFN}_{\varPi^1_{n+2}}(T_0) \ = \ \mathrm{I}{\varPi^1_n} \ \supseteq \ (\mathrm{I}\varPi^1_n)^{-} \ = \ \mathrm{RFN}_{\varSigma^1_{n+1}}(T_0), \end{align} $$
$$ \begin{align} \mathrm{RFN}_{\varPi^1_{n+2}}(T) \ = \ \mathrm{TI}_{\varPi^1_n}(\varepsilon_0) \ \supseteq \ \mathrm{TI}_{\varPi^1_n}(\varepsilon_0)^{-} \ = \ \mathrm{RFN}_{\varSigma^1_{n+1}}(T). \end{align} $$
More in general, if
$T_0$
is axiomatized by a
$\varPi ^1_{k+2}$
sentence, then the above relations hold for all
$n\geq k+1$
.
Proof We sketch a proof of (6).
1. From (
$\varSigma ^1_{n+1}$
)
$\varPi ^1_{n+2}$
uniform reflection to (lightface)
$\varPi ^1_n$
transfinite induction. Note that for a
$\varPi ^1_n$
formula
$\varphi (x)$
, the formula
$$\begin{align*}\psi(z)\ =_{\mathrm{def}}\ \forall x\,(\forall y\prec x\, \varphi(y)\rightarrow \varphi(x))\rightarrow \forall x\prec \omega_z\, \varphi(x) \end{align*}$$
is
$\varSigma ^1_{n+1}$
within
$\mathsf {RCA}_0$
(by simple quantifier manipulations).
1.1. Let us consider the lightface case. Suppose that
$\varphi (x)$
has no set parameters. Note that
$\varphi (x)$
may contain free number variables other than x, say
$x_1,\ldots ,x_i$
. We have
Then one can apply (the multivariate version of)
$\varSigma ^1_{n+1}$
uniform reflection, and obtain
$$\begin{align*}T_0 + \mathrm{RFN}_{\varSigma^1_{n+1}}(T) \vdash \forall z\,\forall x_1\cdots \forall x_i\, \psi(z,x_1,\ldots,x_i). \end{align*}$$
1.2. For the boldface version, suppose that
$\varphi (x)$
has parameters
$x_1,\ldots ,x_i$
and
$X_1,\ldots ,X_j$
. Then one must apply (the multivariate version of) uniform reflection to
$$\begin{align*}\forall X_1\cdots\forall X_j\,\psi(z,x_1,\ldots,x_i,X_1,\ldots,X_j), \end{align*}$$
which is
$\varPi ^1_{n+2}$
. Therefore,
and hence
$$\begin{align*}T_0 + \mathrm{RFN}_{\varPi^1_{n+2}}(T)\vdash \forall z\,\forall x_1\cdots \forall x_i\,\forall X_1\cdots\forall X_j\,\psi(z,x_1,\ldots,x_i,X_1,\ldots,X_j). \end{align*}$$
2. From
$\varPi ^1_n$
transfinite induction to
$\varPi ^1_{n+2}$
uniform reflection.
Fix a
$\varPi ^1_2$
axiomatization
$\forall X\,\psi (X)$
of
$T_0$
. Let
$\forall X\,\exists Y\,\varphi (x,X,Y)$
be a
$\varPi ^1_{n+2}$
formula with no free variables other than x. By definition,
$\varphi (x,X,Y)$
is
$\varPi ^1_n$
. We aim to show
Work in
$T_0 +\mathrm {TI}_{\varPi ^1_n}(\varepsilon _0)$
. Suppose that
$\forall X\,\exists Y\,\varphi (\bar x,X,Y)$
is provable in T. By embedding and cut elimination, we obtain a cut-free
$\omega $
-proof of height
$< \varepsilon _0$
of the sequent
$$\begin{align*}\Xi\ =\ \exists X\,\neg \psi(X), \forall X\,\exists Y\, \varphi(\bar x,X,Y). \end{align*}$$
We aim to prove that
$\forall X\,\exists Y\,\varphi (\bar x,X,Y)$
is true. Suppose, towards a contradiction, that there is a set
$X_0$
such that
$\neg \exists Y\, \varphi (x,X_0,Y)$
is true. We are going to argue as in [Reference Leivant13] (cf. also [Reference Ono15, Lemma 4.3]) and note that in order to analyze a cut-free proof of a false
$\varPi ^1_{n+2}$
formula we only need a partial truth predicate for (enough)
$\varPi ^1_n$
formulas.
By the subformula property, every sequent
$\Gamma $
appearing in a cut-free
$\omega $
-proof of
$\Xi $
is of the form
$\Pi ,\Lambda $
, where
$\Pi $
consists of
$\varPi ^1_n$
formulas and
$\Lambda \subseteq \Xi \cup \{\exists Y\, \varphi (\bar x,U,Y)\mid U \text { free variable}\}$
. Call a sequent of this form a
$\Xi $
-sequent. Now, given a cut-free
$\omega $
-proof of height
$< \varepsilon _0$
of a
$\Xi $
-sequent, we prove by
$\varPi ^1_n$
transfinite induction on
$\varepsilon _0$
that:
“For every
$\Xi $
-sequent
$\Pi ,\Lambda $
appearing in such a proof, the formula
$\bigvee \Pi $
is true for any evaluation of the free variables, with the proviso that the eigenvariables of a
$\forall $
-introduction of
$\forall X\,\exists Y\,\varphi (\bar x,X,Y)$
are evaluated by the set
$X_0$
.”
The property in quotation marks can be expressed by a
$\varPi ^1_n$
formula. For this we use a
$\varPi ^1_n$
truth predicate for a sufficiently large class of
$\varPi ^1_n$
formulas, one of the form
$P_{n,m}$
so that both
$\neg \psi (X)$
and
$\varphi (x,X,Y)$
are in
$P_{n,m}$
. Note also that
$\varPi ^1_n$
induction suffices to prove that
$\varPi ^1_n$
formulas are closed under bounded quantifiers, so that the segment “…the formula
$\bigvee \Pi $
is true…” is indeed equivalent to a
$\varPi ^1_n$
formula.
We consider two key cases. Suppose we have an inference of the form
$$\begin{align*}\frac{\Pi,\neg \psi(W),\Lambda}{\Pi,\Lambda,\exists X\,\neg \psi(X)}. \end{align*}$$
Here,
$\neg \psi (W)$
is
$\varPi ^1_1$
and hence
$\varPi ^1_n$
. Given an evaluation of all free variables as above, we want to show that
$\bigvee \Pi $
is true. By possibly extending the evaluation to W, say by the set X, we can assume by the induction hypothesis that
$\bigvee \Pi \lor \neg \psi (X)$
is true. By the assumption
$\forall X\,\psi (X)$
we can clearly rule out
$\neg \psi (X)$
from being true. Hence we are done.
The other interesting case is when we have an inference of the form
$$\begin{align*}\frac{\Pi,\varphi(\bar x,U,V),\Lambda}{\Pi,\Lambda,\exists Y\,\varphi(\bar x,U,Y)}. \end{align*}$$
Fix an evaluation of all variables such that the set variable U is evaluated by the set
$X_0$
. If necessary, we can extend the evaluation to the set variable V, say by the set Y. By the induction hypothesis,
$\bigvee \Pi \lor \varphi (\bar x,X_0,Y)$
is true. On the other hand, from the assumption,
$\varphi (\bar x,X_0,Y)$
is not true. Thereby,
$\bigvee \Pi $
is true.
We now have a contradiction since the
$\Pi $
part of the sequent
$\Xi $
is empty or possibly consisting of
$\exists X\,\neg \psi (X)$
. In each case, the sequent fails to satisfy the required property.
3. From lightface
$\varPi ^1_{n}$
transfinite induction to
$\varSigma ^1_{n+1}$
uniform reflection.
We work in
$T_0 + \mathrm {TI}_{\varPi ^1_n}(\varepsilon _0)^{-}$
. Suppose that
$\exists X\, \forall Y\, \varphi (\bar x,X,Y)$
, where
$\varphi (x,X,Y)$
is
$\varSigma ^1_{n-1}$
, is provable in T. Then we have a cut-free
$\omega $
-proof of height
$< \varepsilon _0$
of the sequent
$$\begin{align*}\Xi\ =\ \exists X\,\neg \psi(X), \exists X\, \forall Y\, \varphi(\bar x,X,Y). \end{align*}$$
We now say that a
$\Xi $
-sequent is one of the form
$\Sigma ,\Lambda $
, where
$\Sigma $
consists of
$\varSigma ^1_{n-1}$
formulas, and
$\Lambda \subseteq \Xi \cup \{\forall Y\, \varphi (\bar x, U, Y)\mid U \text { free variable}\}$
. Suppose, towards a contradiction, that
$\neg \exists X\, \forall Y\, \varphi (x,X,Y)$
. Again, we follow Leivant’s strategy by considering only true
$\varSigma ^1_{n-1}$
formulas in analyzing a cut-free proof of a false
$\varSigma ^1_{n+1}$
formula. As before, every sequent in a cut-free
$\omega $
-proof of
$\Xi $
is a
$\Xi $
-sequent. We want to show that:
“For every
$\Xi $
-sequent
$\Sigma ,\Lambda $
of a cut-free
$\omega $
-proof, the formula
$\bigvee \Sigma $
is true for every evaluation of the free variables.”
A moment’s reflection shows that this can be formalized by a
$\varPi ^1_n$
formula with no set parameters. Note that if we use trees (second order objects) to represent
$\omega $
-proofs, we must quantify over all possible cut-free
$\omega $
-proofs in order to apply lightface
$\varPi ^1_n$
transfinite induction. Let us consider the only key case. Suppose we have an inference of the form
$$\begin{align*}\frac{\Sigma,\varphi(\bar x, U,V),\Lambda }{\Sigma,\Lambda,\forall Y\, \varphi(\bar x,U,Y)} , \end{align*}$$
where V is the eigenvariable, and so does not appear in the lower sequent. Given an evaluation of the free variables by sets
$X,\ldots $
, where X is the evaluation of U, we want to show that
$\bigvee \Sigma (X,\ldots )$
is true. By the induction hypothesis, for any evaluation of the extra variable V, say by the set Y, we have that
$\bigvee \Sigma (X,\ldots )\lor \varphi (\bar x, X,Y)$
is true. By the eigenvariable condition, this implies that
$\bigvee \Sigma (X,\ldots ) \lor \forall Y\, \varphi (\bar x, X,Y)$
is true. By the assumption, we can rule out the case where
$\forall Y\, \varphi (\bar x, X,Y)$
is true, as desired. As before, one obtains a contradiction since the end sequent fails to satisfy the required property.
5.1 Separation results
The local reflection principle
$\mathrm {Rfn}(T)$
for a theory T is the schema consisting of sentences
We now show, under mild assumptions, that the inclusions in Theorem 5.1 are strict. This will be an immediate consequence of the following.
Lemma 5.2. Let
$T_0$
be a
$\varPi ^1_2$
finitely axiomatizable theory extending
$\mathsf {ACA}_0$
and
$n\geq 1$
. Then
$$ \begin{align} T_0 + \mathrm{RFN}_{\varPi^1_{n+2}}(T_0)\not\vdash \mathrm{Rfn}_{\varSigma^1_{n+2}}(T_0). \end{align} $$
If, moreover,
$T_0 + \mathrm {RFN}_{\varSigma ^1_{n+1}}(T_0) + \varSigma ^1_{n+1}$
-
$\mathsf {AC}$
is consistent, then
$$ \begin{align} T_0 + \mathrm{RFN}_{\varSigma^1_{n+1}}(T_0) \not\vdash \mathrm{Rfn}_{\varPi^1_{n+1}}(T_0). \end{align} $$
The same holds with respect to reflection over T instead of
$T_0$
, where T is
$T_0$
plus the schema of full induction.
Proof By using a universal
$\varPi ^1_{n+2}$
formula one can see that, over
$\mathsf {ACA}_0$
, the schema
$\mathrm {RFN}_{\varPi ^1_{n+2}}(T_0)$
can be axiomatized by a
$\varPi ^1_{n+2}$
sentence, call it
$\psi $
. Now,
By the second incompleteness theorem,
$T_0 +\mathrm {RFN}_{\varPi ^1_{n+2}}(T_0)\not \vdash \mathrm {Rfn}_{\varSigma ^1_{n+2}}(T_0)$
. This proves (7).
Let us show (8). By using a universal
$\varSigma ^1_{n+1}$
formula, the schema
$\mathrm {RFN}_{\varSigma ^1_{n+1}}(T_0)$
can be axiomatized in
$\mathsf {ACA}_0$
by a sentence of the form
$\forall x\,\vartheta (x)$
, where
$\vartheta $
is
$\varSigma ^1_{n+1}$
. This formula is not
$\varSigma ^1_{n+1}$
yet. Now, let
$\varphi $
be the
$\varSigma ^1_{n+1}$
sentence obtained by applying choice to
$\forall x\,\vartheta (x)$
. By the consistency assumption,
$T_0 +\{\varphi \}$
is consistent. As before,
By the second incompleteness theorem,
$T_0 +\{\varphi \}\not \vdash \mathrm {Rfn}_{\varPi ^1_{n+1}}(T_0)$
. Note that
$\varphi $
implies
$\forall x\,\vartheta (x)$
, over, say,
$\mathsf {RCA}_0$
. It follows that
$T_0 +\mathrm {RFN}_{\varSigma ^1_{n+1}}(T_0)\not \vdash \mathrm {Rfn}_{\varPi ^1_{n+1}}(T_0)$
.
By combining Theorem 5.1 with Lemma 5.2 we then obtain the following.
Theorem 5.3. Under the hypotheses of Lemma 5.2,
$$ \begin{align} T_0 + \mathrm{I}{\varPi^1_n} \not\vdash (\mathrm{I}\varPi^1_{n+1})^{-}, \end{align} $$
$$ \begin{align} T_0 + (\mathrm{I}\varPi^1_{n+1})^{-} \not\vdash \mathrm{I}{\varPi^1_n}. \end{align} $$
The same holds with respect to
$\mathrm {TI}_{\varPi ^1_n}(\varepsilon _0)$
and
$\mathrm {TI}_{\varPi ^1_{n+1}}(\varepsilon _0)^{-}$
.
Remark 5.4. The proof of Theorem 5.1 shows that
$$\begin{align*}T_0 +(\mathrm{I}{\varPi^1_n})^{--}\vdash \mathrm{Rfn}_{\varSigma^1_{n+1}}(T_0), \end{align*}$$
where
${}^{--}$
denotes the restriction of induction to
$\varPi ^1_n$
formulas with no parameters at all. Hence, we can strengthen (5
$^{\neg }$
) by replacing
$(\mathrm {I}\varPi ^1_{n+1})^{-}$
with its
${}^{--}$
sibling. Similarly,
$$\begin{align*}T_0 + \mathrm{TI}_{\varPi^1_n}(\varepsilon_0)^{--}\vdash \mathrm{Rfn}_{\varSigma^1_{n+1}}(T) \end{align*}$$
and hence
$T_0 +\mathrm {TI}_{\varPi ^1_n}(\varepsilon _0) \not \vdash \mathrm {TI}_{\varPi ^1_{n+1}}(\varepsilon _0)^{--}$
.
Question. Can we drop the assumptions of Lemma 5.2? What is the relation between local reflection, induction, transfinite induction up to
$\varepsilon _0$
, and corresponding parameter free variants
${}^-$
and
${}^{--}$
?
Acknowledgments
I would like to thank the referees for their thorough and detailed reports. The author’s research was supported by the Alexander von Humboldt foundation.
