13

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.

Community
  • 1
Colin McLarty
  • 10,817

1 Answers1

18

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)}$.

Emil Jeřábek
  • 44,710
  • 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
  • 1
    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: http://www.andrew.cmu.edu/user/avigad/Talks/semantic.pdf) – Emil Jeřábek Apr 10 '13 at 12:48
  • 2
    Emil, what would be a reference for Solovay's result? (I couldn't locate it in Hájek-Pudlák.) – Andrés E. Caicedo Sep 24 '13 at 01:34
  • 1
    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
  • Hello. I'm new to this area. Why is $K$ closed under multiplication? And does closedness under multiplication imply that of addition? – Ris Apr 29 '21 at 21:29
  • Because $J$ is closed under $\omega_k$. Just substitute it in and do the math. – Emil Jeřábek Apr 30 '21 at 05:51
  • Sorry but I'm stuck at the math. We should prove $2_k^n \in J \implies 2_k^{n^2} \in J$, but I have no idea how to bound it with $\omega_k$. For $k = 1$, for bounding $2^{n^2}$ in terms of $2^n$, $\omega_1(x) = 2x$ seems too weak. Am I missing something? – Ris May 02 '21 at 18:49
  • You have a wrong definition. $\omega_1(x)=x^{\log x}=2^{(\log x)^2}$. In general, $\omega_k(x)=2^{(\log^{(k)}x)^2}_k$. – Emil Jeřábek May 02 '21 at 19:24
  • Seems like it's different from how Pudlák uses $\omega_k$ in “Cuts, consistency statements, and interpretations”. It seems to coincide with the definition you're referring to if we use $\omega_{k + 2, Pudlák}$ as $\omega_k$, and $\omega_{2, Pudlák}$ as real square. Where can I find the definition you're referring to? – Ris May 02 '21 at 19:54
  • @Ris I see that Pudlák is experimenting with the subscripts (he’s using yet another numbering in the Hájek&Pudlák book). The standard definition is the original one due to Paris and Wilkie, see e.g. https://doi.org/10.1016/0168-0072(87)90066-2 . (They actually define $\omega_k$ for $k\ge2$ in a more cumbersome way: $\omega_k(x)=x^{(\log x)^{(\log\log x)^{.^{.^{.^{\log^{(k)}x}}}}}}$. This has roughly the same rate of growth as the simpler definition I gave above, which is commonly used instead these days.) – Emil Jeřábek May 03 '21 at 07:08
  • Thanks for the reference. By the way I was thinking about the argument for $I\Delta_0 + EXP + \mathrm{Th}_{\Sigma_2^0}(\mathbb{N})$. While proving a variant of Parikh's theorem with compactness, $\Sigma_2^0$ formulas are not absolute for subcuts but by instantiating with a constant(say, $a$), it can be made $\Pi_1^0$, which is downward absolute. But I have no idea how to ensure $a \le 2_k^d$ as in Pudlák's paper. – Ris May 03 '21 at 11:13
  • A $\Sigma_2$ sentence true in $\mathbb N$ has a witness $a\in\mathbb N$, which is automatically included in every cut. In other words, $I\Delta_0+\mathrm{EXP}+\mathrm{Th}{\Sigma_2}(\mathbb N)=I\Delta_0+\mathrm{EXP}+\mathrm{Th}{\Pi_1}(\mathbb N)$ (or even ${}=\mathrm{Th}_{\Pi_1}(\mathbb N)+\mathrm{EXP}$). – Emil Jeřábek May 03 '21 at 11:29
  • Ahh I get it. I was thinking about individual formulas but considered together, they would by equivalent. For the last time, $\mathrm{Con}_\mathrm{PA}$ holds in $J$ because a proof of contradiction $d \in J$ is impossible, because the formulas in $d$ are below than $\Sigma_d^0$, which is absurd because there is a $\Sigma_d^0$ truth predicate. Is this right? – Ris May 03 '21 at 11:47
  • Yes. If you have a truth predicate for all formulas that appear in the proof, you show by induction that all formulas in the proof are true (according to the truth predicate), but the final contradiction is not true. – Emil Jeřábek May 03 '21 at 13:12