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?



How do you prove that Q+Con(PA) can't be interpreted in ACA_0?
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](https://mathoverflow.net/questions/127080/what-metatheory-proves-mathsfaca-0-conservative-over-pa/127084#127084) 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).


