# Is $ACA_0$ + `True Arithmetic exists' interpretable in $ACA$?

Maybe someone here can help me with a question concerning second-order arithmetic. Consider the system $ACA_T := ACA_0 + \exists X \forall x (x \in X \leftrightarrow T(x))$, where $T(x)$ is a $\Pi_1^1$ truth definition for first-order arithmetic (as given e.g. in Takeuti, Proof Theory, p. 183-188). So $ACA_T$ is $ACA_0$ plus a statement that says that the set of (Gödel numbers of) of true arithmetic exists. The question I have is: Is $ACA_T$ interpretable in $ACA$? I know that one can show that the arithmetical consequences of $ACA_T$ are precisely the consequences of $ACA$. But I would like to know whether $ACA_T$ can be directly interpreted in $ACA$.

$\def\aca{\mathit{ACA}}\aca_T$ is finitely axiomatized, hence whenever it is interpretable in some theory, it is also interpretable in its finite subtheory. On the other hand, $\aca$ has full induction, hence it is (uniformly essentially) reflexive, that is, it proves the consistency of all its finite subtheories. It follows that if $\aca$ interpreted $\aca_T$, it would actually prove the consistency of $\aca_T$. (The converse also holds.)
Thus, assuming that your claim that $\aca$ and $\aca_T$ have the same arithmetical consequences is correct, the answer is negative, as $\aca_T$ does not prove its own consistency by Gödel’s theorem.
• Emil's line of reasoning also shows that $ACA_0$ is not interpretable in $PA$, even though they have the same arithmetical consequences. Therefore one can summarize the situation by $\frac{ACA_0}{PA}=\frac{ACA_T}{ACA}$. – Ali Enayat Feb 20 '15 at 13:59
• That’s right. Another such example is that NBG is not interpretable in ZF(C), where I believe the argument was first noticed; and $I\Sigma_1$ is not interpretable in PRA (however, here one needs a more elaborate proof to show that PRA is reflexive). – Emil Jeřábek Feb 20 '15 at 14:09
• That's very interesting! Thanks for the answer! I hope a quick follow-up is ok: the reason I was asking this question is because I need some "weak" set theory in which $ACA_T$ is interpretable and I knew that $ACA$ is interpretable in $KP \omega$ (Kripke-Platek set theory with infinity). So maybe someone has a direct answer to this question: Is $ACA_T$ interpretable in some well-known weak set theory, like $KP \omega$? – user68318 Feb 20 '15 at 21:48
• I’m not very familiar with Kripke–Platek, however, it seems to me that it proves $\aca_T$ under the standard interpretation: show by induction on $n$ that there exists a truth predicate for arithmetical formulas of Gödel number below $n$, and then construct the full truth predicate using $\Sigma_0$-collection. – Emil Jeřábek Feb 20 '15 at 22:43