The formalization of interpretability

The subject of our study as mentioned before is formal theories. The main tool used will be the notion of interpretability. There are many notions of interpretability, so we have to choose one for the default notion. When we talk in this paper about interpretability we refer to the notion of relative interpretability used in [TMR53]. A relative interpretation comprises a translation t and a relativizing formula $\sigma (x)$. t is a translation from the language of T' into the language of T. To every predicate constant Pin the language of T', the translation assigns a formula P^t in the language of T. The relativizing formula $\sigma$ is in the language of T as well. The translation is defined such that:

• t(x=y) is x=y,
• for any other atom one has $t(P(\vec{x}))$ to be $P^t(\vec{x})$,
• t commutes with the Boolean connectives,
• $t(\forall x\alpha)$ is $\forall x(\sigma (x)\rightarrow t(\alpha ))$and consequently $t(\exists x\alpha)$ will be
  $\exists x(\sigma (x)\wedge t(\alpha ))$.

So it will be clear what it means to say that a theory S interprets a theory T, namely S proves every translated theorem of T for some translation. This will be abbreviated by stating $S\rhd T$. Now if a theory T is strong enough one can do sufficient coding and hence talk within the theory T itself about interpretability. So within a theory one can formalize statements like $\alpha \rhd \beta$, stating ``$T+\alpha$ interprets $T+\beta$''. The intuitive reading should be something like ``for some translation, $T+\alpha$ proves the translation of every theorem of $T+\beta$''. And actually like this it can be formalized. For an extensive treatment one can see for example [JdJ98], [Vis97] or [Ber90]. If we are not too concerned about correct notation, we can think of formalized interpretability as the following $\Sigma^0_3$-sentence:

$$\alpha \rhd \beta \Leftrightarrow \exists J(\Box_T(\alpha \ri... ...(y)\rightarrow \Box_T(\alpha \rightarrow y^J))).\ \ \ \ \ \ (+)$$

In this sentence ${\mathit Ax}_T$ is the formula expressing the fact: ``y is the code of an axiom of T''. The $\Box_T$ is a notion expressing provability in T. We will always use an intensional translation of the notion of provability. That is, not just any notion which externally happens to be the same as provability, but a notion in which the meaning of provability is really coded. See for example [Boo93]. It is only important that the provability notion will generate the Hilbert-Bernays conditions (also called Löb conditions) and consequently all of Löb's provability logic. There are provability predicates known for which the Hilbert-Bernays conditions are not derivable and for which the second incompleteness theorem of Gödel does not hold (see for example [Sha94] or [Vis89]), but we will not consider them. The J in (+) is the interpretation itself, comprising a translation from the one language into the other as well as a relativizing formula, defining the domain of the interpreted theory. If $T\rhd S$ is true, one has a uniform method of finding a model of S in any model of T. Thinking in terms of submodels can be very useful for acquainting oneself with some intuition on arithmetically valid principles. For example $S\rhd R \wedge R\rhd T\rightarrow S\rhd T$ can be thought of as a reflection of the following argument: ``If in any model of S one can define a model of R, and if in any model of R one can define a model of T, one can consequently define in any model of S, a model of T.''