First-order parts and conservation

Let $\sigma$ be an $\mathcal L_1$ sentence not provable in $S$. Then $S + \neg \sigma$ is consistent, and has a countable model $M$. Let $\mathcal N$ be an ω-extension of $M$ satisfying $T$. Since $\sigma$ has no set variables, $\mathcal N \models \neg \sigma$. So $T + \neg \sigma$ has a model, and $T$ does not prove $\sigma$.

$\mathsf{ACA}_0$ proves the induction scheme for arithmetic formulas, in particular for all formulas of $\mathcal L_1$ (Definition 1.1 of “Arithmetic comprehension” and Proposition 1.3 of “The language and models of second-order arithmetic”). Conversely, let $M$ be a countable model of $\mathrm{PA}$, and let $\mathcal D$ be the class of subsets of $M$ definable in $M$ by a formula of $\mathcal L_1$ with parameters in $M$. Let $\mathcal N = (M, \mathcal D)$. We show $\mathcal N \models \mathsf{ACA}_0$, which proves the theorem by Proposition 3.3.

The basic axioms hold since $M$ satisfies them. Let $\varphi(n)$ be an arithmetic formula with set parameters $X_1, \dots, X_k \in \mathcal D$ and number parameters in $M$, and let $\delta_i(u)$ be an $\mathcal L_1$ formula with parameters defining $X_i$ in $M$. Replacing every atomic formula $t \in X_i$ by $\delta_i(t)$ gives an $\mathcal L_1$ formula $\varphi^*$ with parameters in $M$, and for every $n \in M$, $\mathcal N \models \varphi(n)$ if and only if $M \models \varphi^*(n)$, by induction on $\varphi$. So the set defined by $\varphi$ in $\mathcal N$ is defined by $\varphi^*$ in $M$, and belongs to $\mathcal D$: arithmetic comprehension holds. For the same reason, $\Sigma^0_1$ induction in $\mathcal N$ reduces to induction in $M$ for $\varphi^*$, which holds in $\mathrm{PA}$.

Let $\varphi_i$ and $\psi_i$ be $\Sigma^0_1$ and $\Pi^0_1$ formulas with parameters in $\mathcal M$ defining $X_i$. Write $\theta = \exists y\, \delta$ with $\delta$ bounded, and put $\delta$ in negation normal form, so that negations only apply to atomic formulas. Replace every atomic formula $t \in X_i$ by $\varphi_i(t)$, and every negated atomic formula $t \notin X_i$ by $\neg \psi_i(t)$, a $\Sigma^0_1$ formula. The result $\delta'$ has parameters in $\mathcal M$, and is equivalent to $\delta$ in $\mathcal M'$, since the replaced formulas are equivalent there. It is built from $\Sigma^0_1$ formulas by $\wedge$, $\vee$ and bounded quantifiers, so by Lemma 1.3, applied in $\mathcal M$, which satisfies $\mathsf B\Sigma^0_1$, it is equivalent in $\mathcal M$ to a $\Sigma^0_1$ formula $\delta^*$. The equivalence involves no $X_i$, so it also holds in $\mathcal M'$. Let $\theta^* = \exists y\, \delta^*$. For a $\Pi^0_1$ formula, apply the result to its negation. If $\mathcal M$ has no sets, the formulas $\varphi_i, \psi_i$ and the result are formulas of $\mathcal L_1$.

$\mathsf{RCA}_0$ proves $\Sigma^0_1$ induction, in particular for formulas of $\mathcal L_1$. Conversely, let $M$ be a countable model of $\mathrm I\Sigma_1$, and $\mathcal D$ the class of sets $\Delta_1$-definable in $M$. By Theorem 1.5, $M$ satisfies $\Sigma_1$ collection. Let $\mathcal N = (M, \mathcal D)$. Every formula with parameters in $\mathcal N$ uses finitely many sets of $\mathcal D$, so Lemma 3.5 applies to it.

• Basic axioms: they hold in $M$.
• $\Sigma^0_1$ induction: let $\theta(x)$ be $\Sigma^0_1$ with parameters in $\mathcal N$, and $\theta^*$ the $\Sigma_1$ formula of $\mathcal L_1$ given by the lemma. Induction holds in $M$ for $\theta^*$, hence in $\mathcal N$ for $\theta$.
• $\Delta^0_1$ comprehension: let $\varphi$ be $\Sigma^0_1$ and $\psi$ be $\Pi^0_1$, with parameters in $\mathcal N$, such that $\mathcal N \models \forall n\, (\varphi(n) \leftrightarrow \psi(n))$. The lemma gives $\varphi^*$ in $\Sigma_1$ and $\psi^*$ in $\Pi_1$, both formulas of $\mathcal L_1$ that define the same set $X$ in $M$. So $X \in \mathcal D$, and $\mathcal N \models \forall n\, (n \in X \leftrightarrow \varphi(n))$.

So $\mathcal N \models \mathsf{RCA}_0$, and Proposition 3.3 concludes.

Suppose the conclusion fails for every $k$. Add a set constant $C$ to the language, and let $\gamma_k$ be the sentence $\forall Y\, (Y \leq_T C^{(k)} \rightarrow \neg G(C, Y))$. For each $k$, $\mathsf{ACA}_0 + F(C) + \gamma_k$ is consistent. Since $\mathsf{ACA}_0$ proves $\gamma_{k+1} \rightarrow \gamma_k$, every finite subset of $\mathsf{ACA}_0 + F(C) + \{ \gamma_k : k \in \nat \}$ is consistent, so the whole theory has a model $\mathcal M = (M, \mathcal S, C)$ by compactness.

Let $\mathcal S'$ be the class of sets in $\mathcal S$ definable in $\mathcal M$ by an arithmetic formula with set parameter $C$ and number parameters, and $\mathcal M' = (M, \mathcal S')$. Then $\mathcal M' \models \mathsf{ACA}_0$: a set defined by an arithmetic formula with parameters in $\mathcal S'$ is, after substitution of their definitions, defined by an arithmetic formula with parameter $C$; it exists in $\mathcal S$ by arithmetic comprehension in $\mathcal M$, so it belongs to $\mathcal S'$; induction holds since $\mathcal S' \subseteq \mathcal S$.

The formula $F(C)$ is arithmetic and holds in $\mathcal M$, so it holds in $\mathcal M'$. Let $Y \in \mathcal S'$, defined by a $\Sigma^0_k$ formula with parameter $C$, for some standard $k$. By the formalized Post theorem, $\mathcal M \models Y \leq_T C^{(k)}$, so $\mathcal M \models \neg G(C, Y)$ by $\gamma_k$, and $\mathcal M' \models \neg G(C, Y)$. Hence $\mathcal M' \models F(C) \wedge \forall Y\, \neg G(C, Y)$, and $\mathsf{ACA}_0$ does not prove $\forall X\, (F(X) \rightarrow \exists Y\, G(X, Y))$, contrary to the hypothesis.

Let $F(X)$ be “the column $X^{[0]}$ is non-empty”, and $G(X, Y)$ be ”$Y$ codes a sequence $Y_0, \dots, Y_n$ with $Y_0 = X^{[1]}$, $Y_{i+1} = Y_i'$, where $n$ is the least element of $X^{[0]}$”. Both are arithmetic, and $\mathsf{ACA}_0'$ proves $\forall X\, (F(X) \rightarrow \exists Y\, G(X, Y))$. If $\mathsf{ACA}_0$ proved it, then for some $k$ it would prove the version with $Y \leq_T X^{(k)}$, and this version would hold in the ω-model $\mathcal P(\nat)$. Take $X$ with $X^{[0]} = \{ k + 1 \}$ and $X^{[1]} = \emptyset$; then $X \equiv_T \emptyset$, and a solution $Y$ computes $\emptyset^{(k+1)}$ while $Y \leq_T X^{(k)} \equiv_T \emptyset^{(k)}$, which contradicts the jump theorem.