# What metatheory proves $\mathsf{ACA}_0$ conservative over PA?

Simpson's book shows $\mathsf{ACA}_0$ is conservative over $\mathsf{PA}$ in the natural way by model theory using definable subsets. Of course, $\mathsf{ACA}_0$ being conservative over PA is interesting even apart from consistency strength. So one might not be explicit about the metatheory. And I am sure it is not a strong one.

But I am curious to know the exact logic of this argument.

-

The conservativity of $\mathrm{ACA}_0$ over $\mathrm{PA}$ is provable in $I\Delta_0+\mathit{SUPEXP}$ by a cut elimination argument. It is not provable in $I\Delta_0+\mathit{EXP}$, since $\mathrm{ACA}_0$ has superexponential speedup over $\mathrm{PA}$ (a result attributed to Solovay, Pudlák, and Friedman).

EDIT: Let me briefly sketch a proof of the speedup theorem here.

Theorem:

1. $I\Delta_0+\mathit{EXP}\nvdash\mathrm{Con}_\mathrm{PA}\to\mathrm{Con}_{\mathrm{ACA}_0}$.

2. For any $k$, there are true $\Sigma^0_1$-sentences $\phi$ such that $l_\mathrm{PA}(\phi)\ge2_k^{l_{\mathrm{ACA}_0}(\phi)}$, where $l_T(\phi)$ denotes the smallest Gödel number of a $T$-proof of $\phi$, and $2_k^x$ is the $k$-times iterated exponential of $x$. Consequently, the ($\Sigma^0_1$-)conservativity of $\mathrm{ACA}_0$ over $\mathrm{PA}$ is not provable in $I\Delta_0+\mathit{EXP}+\mathrm{Th}_{\Sigma^0_2}(\mathbb N)$.

Proof:

For 1, a variant of Parikh’s theorem shows that if $I\Delta_0+\mathit{EXP}\vdash\mathrm{Con}_\mathrm{PA}\to\mathrm{Con}_{\mathrm{ACA}_0}$, there is a constant $k$ such that $$\tag{*}I\Delta_0\vdash p\le\log^{(k)}(x)\land\mathrm{Proof}_{\mathrm{ACA}_0}(p,\ulcorner\bot\urcorner)\to\exists q\le x\,\mathrm{Proof}_{\mathrm{PA}}(q,\ulcorner\bot\urcorner).$$ Working in $\mathrm{ACA}_0$, one can define a cut $I(n)$ consisting of those $n$ such that there exists a truth-predicate for $\Sigma^0_n$-sentences satisfying Tarski’s definition (the inductive clauses can be described by an arithmetical formula, hence $I$ is $\Sigma^1_1$-definable). Using the method of shortening of cuts, let $J(n)$ be a cut $\mathrm{ACA}_0$-provably closed under $\omega_k$ and included in $I$. We have $$\mathrm{ACA}_0\vdash(I\Delta_0+\Omega_k+\mathrm{Con}_\mathrm{PA})^J.$$ Let $K(n)\iff J(2_k^n)$. Then $K$ is a cut closed under multiplication, and we have $$\mathrm{ACA}_0\vdash(I\Delta_0+\mathrm{Con}_{\mathrm{ACA}_0})^K$$ using $(*)$, which contradicts a suitable version of Gödel’s incompleteness theorem.

For 2, let $\psi$ be the $\Pi^0_1$-sentence $$\forall s\in\Sigma^0_1\forall x,p\,\bigl(p\le\log^{(k)}(x)\land\mathrm{Proof}_{\mathrm{ACA}_0}(p,s)\to\exists q\le x\,\mathrm{Proof}_{\mathrm{PA}}(q,s)\bigr)$$ expressing that $\mathrm{ACA}_0$ has no speedup faster than $2_k^x$ over $\mathrm{PA}$ (for $\Sigma^0_1$-sentences). By the same argument as in 1, we show $$\mathrm{ACA}_0+\psi\vdash(I\Delta_0+\mathrm{Con}_{\mathrm{ACA}_0+\psi})^K,$$ hence $\mathrm{ACA}_0\vdash\neg\psi$ by Gödel’s theorem. In particular, $\psi$ is false, hence $\mathrm{ACA}_0$ has speedup faster than $2_k^x$ over $\mathrm{PA}$ for some $\Sigma^0_1$-sentences $\phi$.

One can construct an explicit such sentence, as well as avoid the appeal to the $\Sigma^0_1$-soundness of $\mathrm{ACA}_0$ at the end of the proof, by defining $$\vdash\phi\leftrightarrow\exists x,p\,\bigl(p\le\log^{(k)}(x)\land\mathrm{Proof}_{\mathrm{ACA}_0}(p,\ulcorner\phi\urcorner)\land\forall q\le x\,\neg\mathrm{Proof}_{\mathrm{PA}}(q,\ulcorner\phi\urcorner)\bigr)$$ using self-reference, and working with $\psi=\neg\phi$.

Notice that there is nothing particularly specific to $\mathrm{PA}$ in the proof. In general, if $T$ is a consistent sequential theory in a finite language, axiomatized by finitely many axioms and axiom schemata (allowing for all formulas with parameters, such as the induction schema of $\mathrm{PA}$), and $T^+$ is its “second-order” conservative extension with first-order comprehension axioms, and the schemata of $T$ replaced with the corresponding $\Pi^1_1$-sentences, then the speedup theorem holds with $T$ and $T^+$ in place of $\mathrm{PA}$ and $\mathrm{ACA}_0$. Particular examples of such theories are $\mathrm{ZF(C)}$ and $\mathrm{GB(C)}$.

-
Nice. And this will also do for the proof that $\mathsf{GB}$ is conservative over $\mathsf{ZF}$, right? –  Colin McLarty Apr 10 '13 at 12:35
Yes. The upper bound does not use anything particular about PA, it works for appropriate two-sorted extensions of pretty much arbitrary recursively axiomatized theories. The lower bound is more delicate, but it is known to hold for GB and ZF as well. (This is not necessarily true for other similar conservation results: the conservativity of $\mathrm{WKL}_0$ over $I\Sigma_1$ incurs no superpolynomial speedup, for instance. This is discussed in this talk by Avigad: andrew.cmu.edu/user/avigad/Talks/semantic.pdf) –  Emil Jeřábek Apr 10 '13 at 12:48
Emil, what would be a reference for Solovay's result? (I couldn't locate it in Hájek-Pudlák.) –  Andres Caicedo Sep 24 '13 at 1:34
Hmm. I see now that the result is variously attributed to Solovay, Pudlák, and Friedman. Solovay’s account may well be unpublished; Pudlák gives the argument for ZF and GB in “Cuts, consistency statements, and interpretations”, JSL 50 (1985), 423–441. –  Emil Jeřábek Sep 30 '13 at 11:36
@EmilJeřábek Thank you! –  Andres Caicedo Sep 30 '13 at 16:15