Harrington's conservation theorem

Let $\forall X\, \varphi(X)$ be a $\Pi^1_1$ sentence, with $\varphi$ arithmetic, not provable in $S$. A countable model $\mathcal M$ of $S + \exists X\, \neg \varphi(X)$ contains a set $A$ with $\mathcal M \models \neg \varphi(A)$. Let $\mathcal N$ be an ω-extension of $\mathcal M$ satisfying $T$. Then $A$ belongs to $\mathcal N$, and $\mathcal N \models \neg \varphi(A)$ since $\varphi$ is arithmetic. So $T$ does not prove $\forall X\, \varphi(X)$.

Write $F = \exists y\, \delta(x, y, X)$ with $\delta$ bounded. By induction on $\delta$, there is a term $p(x, y)$ such that, for all values of the bounded variables within their bounds, every term $t$ of an atomic formula $t \in X$ of $\delta$ has a value less than $p(x, y)$: terms are polynomials with non-negative coefficients, which are monotone, so it suffices to replace each bounded variable by its bound. Let $\delta(x, y, \sigma)$ be the formula obtained by replacing $t \in X$ by "$t < |\sigma| \wedge \sigma(t) = 1$", and

It is bounded and monotone in $\sigma$. If $|\sigma| \geq p(x, y)$ and $\sigma = G \uh |\sigma|$, then $\delta(x, y, G)$ and $\delta(x, y, \sigma)$ have the same truth value, by induction on $\delta$, since every atomic formula $t \in X$ is evaluated at some $t < p(x, y)$, where $\sigma$ and $G$ agree. If $\mathcal M \cup \{ G \} \models \delta(x, y, G)$, take $k$ larger than $y$ and $p(x, y)$. Conversely, if $H(x, G \uh k)$ holds with witness $y$, then $\delta(x, y, G)$ holds.

Let $S \in \mathbb P$. For each string $\sigma$ of length $n$, the tree $S^\sigma = \{ \tau \in S : \tau \preceq \sigma \vee \sigma \preceq \tau \}$ belongs to $\mathcal S$ by $\Delta^0_1$ comprehension, and has at most one string of length $n$. Suppose that none of them is $\mathcal M$-infinite: every $\sigma$ of length $n$ has some $m$ such that $S^\sigma$ has no string of length $m$. This is a bounded quantification of a $\Sigma^0_1$ formula, so by $\mathsf B\Sigma^0_1$, which holds in $\mathcal M$, there is $m^*$, which we may take at least $n$, such that every $S^\sigma$ has no string of some length $m < m^*$; since $S^\sigma$ is closed under prefixes, it has no string of length $m^*$ either. Then $S$ has no string $\rho$ of length $m^*$, since $\rho$ would belong to $S^{\rho \uh n}$. This contradicts the $\mathcal M$-infiniteness of $S$. So some $S^\sigma$ is $\mathcal M$-infinite; it belongs to $\mathbb P$, and its only string of length $n$ is $\sigma$, so it belongs to $D_n$.

Let $S \in \mathbb P$. For every string $\sigma$ of length $b$, let

It belongs to $\mathcal S$ by $\Delta^0_1$ comprehension, and it is a tree, since the condition is inherited by prefixes. The set $U$ of strings $\sigma$ of length $b$ such that $S_\sigma$ is $\mathcal M$-infinite is defined by a $\Pi^0_1$ formula, and contains the string $1^b$, since $S_{1^b} = S$. Code the strings of length $b$ so that the numerical order is the lexicographic order. By $\mathsf L\Pi^0_1$, which holds in $\mathcal M$ by Proposition 1.6, $U$ has a lexicographically least element $\sigma$. We show $S_\sigma \in D_{F, b}$; it belongs to $\mathbb P$ since $\sigma \in U$. Let $a < b$.

• If $\sigma(a) = 0$, then $\Psi_{S_\sigma}(a)$ holds by definition of $S_\sigma$.
• If $\sigma(a) = 1$, let $\tau$ be the string of length $b$ that agrees with $\sigma$ below $a$, has $\tau(a) = 0$, and $\tau(i) = 1$ for $a < i < b$. It is lexicographically smaller than $\sigma$, so $\tau \notin U$: there is $m$ such that $S_\tau$ has no string of length $m$. Let $\rho \in S_\sigma$ with $|\rho| = m$. The string $\rho$ satisfies the conditions of $S_\sigma$ at the positions below $a$, which are those of $S_\tau$ below $a$, and $S_\tau$ has no other condition except at $a$. Since $\rho \notin S_\tau$, the condition at $a$ fails: $H(a, \rho \uh k)$ for some $k \leq m$. So $\Phi_{S_\sigma}(a)$ holds, with this $m$.

Let $F(x, G)$ be a $\Sigma^0_1$ formula with parameters in $\mathcal M$ and $G$, such that $F(0, G)$ and $\forall x\, (F(x, G) \rightarrow F(x+1, G))$ hold in $\mathcal M \cup \{ G \}$, and suppose $\neg F(b, G)$ for some $b \in M$. Let $S = S_j \in D_{F, b+1}$, and $H$ as in Lemma 4.3. For $a \leq b$, we claim that $F(a, G)$ holds if and only if $\mathcal M \models \Phi_S(a)$. If $\Phi_S(a)$, then $F(a, G)$ by the remark before Lemma 4.5 and Lemma 4.3. If $F(a, G)$, then $\Psi_S(a)$ fails, so $\Phi_S(a)$ holds since $S \in D_{F, b+1}$.

Hence, in $\mathcal M$: $\Phi_S(0)$ holds, $\Phi_S(a) \rightarrow \Phi_S(a+1)$ for every $a < b$, and $\neg \Phi_S(b)$. The formula $a \leq b \rightarrow \Phi_S(a)$ is $\Sigma^0_1$ with parameters in $\mathcal M$, so $\Sigma^0_1$ induction in $\mathcal M$ gives $\Phi_S(b)$: a contradiction.

Every set of $\mathcal S$, and $G$, is defined by a bounded formula, so belongs to $\mathcal M[G]$. By Lemma 4.6 and Theorem 1.5, $\mathcal M \cup \{ G \}$ satisfies $\mathsf B\Sigma^0_1$. So Lemma 3.5 applies to $\mathcal M \cup \{ G \}$ and finitely many sets of $\mathcal M[G]$: every $\Sigma^0_1$ or $\Pi^0_1$ formula with parameters in $\mathcal M[G]$ is equivalent in $\mathcal M[G]$ to a formula of the same class with parameters in $\mathcal M \cup \{ G \}$. As in the proof of Theorem 3.6, $\Sigma^0_1$ induction in $\mathcal M[G]$ reduces to Lemma 4.6, and $\Delta^0_1$ comprehension holds because a set $\Delta^0_1$-definable with parameters in $\mathcal M[G]$ is $\Delta^0_1$-definable with parameters in $\mathcal M \cup \{ G \}$. Finally, “every initial segment of $G$ belongs to $T$” is an arithmetic statement about $G$ and $T$, true by construction.

Let $\mathcal M_0$ be a countable model of $\mathsf{RCA}_0$. We build countable ω-extensions $\mathcal M_0 \subseteq \mathcal M_1 \subseteq \cdots$, all models of $\mathsf{RCA}_0$, as follows. Fix a bijection $i \mapsto (i_0, i_1)$ from $\nat$ to $\nat^2$ with $i_0 \leq i$. At step $i$, consider the $i_1$-th set of $\mathcal M_{i_0}$, in a fixed enumeration of its sets. If it is an $\mathcal M_i$-infinite tree $T$, let $\mathcal M_{i+1} = \mathcal M_i[G]$ for a path $G$ through $T$ given by the construction above, applied to $\mathcal M_i$; otherwise let $\mathcal M_{i+1} = \mathcal M_i$. By Lemma 4.7, every $\mathcal M_{i+1}$ is a model of $\mathsf{RCA}_0$; it is countable, since its sets are defined by formulas with parameters in the countable structure $\mathcal M_i \cup \{ G \}$.

Let $\mathcal N$ be the union: same first-order part, and the union of the second-order parts. Every instance of the axioms of $\mathsf{RCA}_0$ in $\mathcal N$ has finitely many set parameters, all in some $\mathcal M_i$, and is arithmetic apart from the conclusion of comprehension; it holds in $\mathcal M_i$, with the same meaning, and the set given by comprehension in $\mathcal M_i$ belongs to $\mathcal N$. So $\mathcal N \models \mathsf{RCA}_0$. If $T \in \mathcal N$ is an infinite tree in the sense of $\mathcal N$, it is the $i_1$-th set of some $\mathcal M_{i_0}$, and it is infinite in the sense of $\mathcal M_i$ at step $i$, since this is arithmetic; so a path through $T$ was added at step $i$, and it belongs to $\mathcal N$. So $\mathcal N \models \mathsf{WKL}_0$.