The theory $\mathrm{ACA}_0$ is not reflexive (because it is finitely axiomatisable and cannot prove its own consistency). So how, if at all, is it possible to prove that $\mathrm{Q+Con(PA)}$ cannot be interpreted in $\mathrm{ACA}_0$?

(I am assuming that for an interpretation of the second-order language of arithmetic, the domain of the number variables must be interpreted to be a set of numbers which is definable without parameters.)

Edit: I believe this is the answer. Because $\mathrm{ACA}_0$ can prove the $\Sigma^{0}_{1}$-completeness of $\mathrm{Q}$. So if the relativisation of $\mathrm{Q+Con(PA)}$ to some definable class model of $\mathrm{Q}$ were provable in $\mathrm{ACA}_0$, then $\mathrm{Con(PA)}$ would also be provable in $\mathrm{ACA}_0$, but this is impossible by Gödel's second incompleteness theorem. Is this correct?


Firstly, your proposed reasoning does not work since $Con(PA)$ is a $\Pi^0_1$ statement.

Secondly, your parenthetical assumption is not in accordance with the general meaning of interpretations, and the result is provable without this assumption.

The fact that $Q + Con(PA)$ is not interpretable in $ACA_0$ is a consequence of a deep result of Pavel Pudlák.

To establish the failure of interpretabilty, one first shows that if $ACA_0$ interprets a model of $Q+Con(PA)$, then $ACA_0$ will be able to define a cut (i.e., a set of numbers containing $0$ and closed under successors) that is a model of $Con(PA)$. This part follows from the fact that for any two interpretations of $Q$ in $ACA_0$, $ACA_0$ can define cuts $A$ and $B$ in each interpretation, and an isomorphism between $A$ and $B$.

However, $ACA_0$ "knows" that $Con(PA)$ iff $Con(ACA_0)$, since this equiconsistency is already provable in a fragment of $PA$, namely superexponential arithmetic (as explained in this post by Emil Jeřábek).

Then, and here is the hard part of the argument, one invokes the theorem, established by Pudlák , that no sequential theory containing $Q$ can prove its own consistency on a definable cut. This result of Pudlák is a generalization of Gödel's second incompleteness theorem, and appears as Theorem 2.1 of the following paper:

P. Pudlák, Cuts, consistency statements, and interpretations, Journal of Symbolic Logic, 1985 (pp.423-441).


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.