How do you prove that Q+Con(PA) can't be interpreted in ACA_0?

Question

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?

Answer 1

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