Is every recursively axiomatizable and consistent theory interpretable in the true arithmetic (TA)?

Question

I am looking for a scholarly text that discusses this issue in detail.

Answer 1

The answer is yes. I believe the following is best attributed to Feferman 1960; more generally, look up "arithmetized completeness theorem" (which is annoyingly different from the arithmetic completeness theorem, an unrelated result in modal logic).

---

First, suppose $T$ is a r.e. theory and $\mathsf{PA}$ (not $\mathsf{TA}$, I'm starting small) proves that $T$ is consistent. Godel's completeness theorem is somewhat effective: every consistent theory has a model computable relative to the Turing jump of (or indeed much less) that theory. Moreover, this effective version of the completeness theorem is provable inside $\mathsf{PA}$ in an appropriate sense. In particular, and utilizing Post's theorem:

Since $\mathsf{PA}$ proves that $T$ is consistent, there is a specific formula $\varphi_T$ which $\mathsf{PA}$ proves defines a model of $T$.

What if $\mathsf{PA}$ doesn't prove that $T$ is consistent? Well, we can still whip up the formula $\varphi_T$ as above, it's just that $\mathsf{PA}$ only conditionally proves that it defines a model of $T$:

More generally, for each r.e. theory $T$ there is a formula $\varphi_T$ such that $\mathsf{PA}$ proves "If $T$ is consistent then $\varphi_T$ defines a model of $T$."

Now we bring in $\mathsf{TA}$. If $T$ is truly consistent, then $\mathsf{PA}+Con(T)\subseteq\mathsf{TA}$ and so in particular $\mathsf{TA}$ proves "$\varphi_T$ defines a model of $T$."

Answer 2

This answer complements the one given by Noah Schweber.

The arithmetized completeness theorem was first proved in the seminal logic text Grundlagen der Mathematik (1928) written by Hilbert and Bernays. Later Kleene (in his textbook Introduction to Metamathematics) showed that the complexity of the interpretation can be fine-tuned to $\Delta_2$. By modern standards, Kleene's refinement is straightforward to establish with the use of (1) Henkin's proof of the completeness theorem, and (2) the fact that the proof of König's tree lemma shows that every infinite recursive binary tree has a $\Delta_2$ infinite branch. This connection to Henkin's proof goes back to the Feferman paper specified in the answer by Noah Schweber. As shown by Hájek & Pudlák (in the text specified by Gro-Tsen in the comment to Schweber's answer) the complexity can be further refined.

It is worth mentioning that, as proved by Orey, if $T$ is a recursively enumerable theory with the property PA can prove $\mathrm{Con}(T_0$) for every finite subtheory $T_0$ of $T$, then PA can interpret the whole of $T$ (this was dubbed by Feferman as Orey's compactness theorem).

For references and a scholarly treatment of the origin of the arithmetized completeness theorem, see this paper by Walter Dean. An expository talk on the relationship between interpretability and the arithmetized completeness theorem, given by Taishi Kurahashi, can be found here.

Answer 3

The other answers are enough to answer the question as given. However, let me point out for the record that using the arithmetized completeness theorem over PA is quite an overkill. We can make do with Robinson’s arithmetic, employing Solovay’s technique of shortening of cuts:

Theorem (“interpretation existence lemma”). If $T$ is a recursively axiomatized theory, then $T$ is interpretable in $\mathsf Q+\mathrm{Con}_T$, and even in $\mathsf Q+\{\mathrm{Con}_{T\restriction n}:n\in\mathbb N\}$.

Here, $T\restriction n$ denotes the theory axiomatized by the axioms of $T$ with Gödel number $\le n$ (under any fixed recursive axiomatization of $T$; the choice does not matter).

In particular, any consistent recursively axiomatized theory is interpretable in an arithmetical theory axiomatized by a single true $\Pi_1$ sentence.

See Visser [1] for a thorough discussion of even more sophisticated versions of the interpretation existence lemma. (NB: the $\mathsf Q+\{\mathrm{Con}_{T\restriction n}:n\in\mathbb N\}$ above is essentially what’s denoted $\mho_{*,\infty}(T)$ in [1].)

Reference

[1] Albert Visser, The Interpretation Existence Lemma, in: Feferman on Foundations (G. Jäger, W. Sieg, eds.), Outstanding Contributions to Logic, vol 13., Springer, 2018, pp. 101–144, doi 10.1007/978-3-319-63334-3_5.