Interpretations

1. Introduction

The Gödel incompleteness theorems do not just apply to arithmetic, but they apply to any formal theory that interprets arithmetic. The idea of interpretation is a very difficult one to pin down, perhaps because there is not one single idea here. In a more advanced treatment, interpretations may be best looked at in the language of category theory (when they are arrows in a category of theories) but this also begs questions as well as solving some.

This web page will try to make a few short and simple definitions and observations on interpretations. Quite a lot of the material here is simplified or over-simplified and many proofs will be omitted.

2. The idea of an interpretation

One formal theory $T$ interprets another theory $S$ if there is some faithful way of translating the expressions and statements of $S$ in such a way that all deductions in $S$ can be performed on their translations in $T$ . This is a very general idea an one that is difficult to pin down and define precisely. There are two very different ideas: one is to define interpretations in terms of the syntax of the theories and the other is to define them in terms of their semantics or models.

Whatever precise definition is used we will use the notation $i : S ⟿ T$ to mean that $i$ is an interpretation of the theory $S$ in the theory $T$ and $θ^{i}$ for the translation of $θ$ under $i$ . The $i$ has low precidence, so $\neg (θ \land ψ)^{i}$ means $(\neg (θ \land ψ))^{i}$ .

At the most general level of all, we might imagine $T$ and $S$ are formal systems whose provable utterances are strings of symbols $τ$ , $σ$ from alphabets $A_{T}$ and $A_{S}$ . It will be convenient to assume that these alphabets are finite, as they can be by encoding each symbol as some string of $0$ s and $1$ s such as $100 \dots 0$ fo a certain number of $0$ s. Then there is a notion of computability on strings from these alphabets (for example by encoding strings as numbers) and notions of provability $T ⊢ τ$ and $S ⊢ σ$ . For a syntactic idea of interpretation we could define an interpretation $i : S ⟿ T$ to be a recursive (i.e. computable) function $i (σ) = τ$ taking strings of symbols $σ$ from $A_{S}$ to strings of symbols $σ^{i}$ from $A_{T}$ . We'll require a couple of things for this interpretation. First, the translations of all string provable in $S$ must be provable in $T$ , that is

whenever $S ⊢ σ$ then $T ⊢ σ^{i}$

Also the theory $S$ will contain some version of propositional logic (in all cases of interest $S$ will in fact be a first order theory) and hence has a connective $\to$ for implies. We require also that,

if $T ⊢ (ρ \to τ)^{i}$ and $T ⊢ ρ^{i}$ then $T ⊢ τ^{i}$ .

With this given, the Gödel incompleteness theorems apply to the theory $T$ that interprets $DOR$ or other such theories. We still need $T$ to be consistent and recursive, but the best way to describe a theory being recursive in general is to say that its set of theorems form a recursively enumerable (r.e.) set. Here is the first theorem.

Theorem.

Suppose $i : DOR ⟿ T$ is a recursive intepretation as above. Suppose that the set $\{τ: T ⊢ τ\}$ of theorems of $T$ is r.e. Suppose also that $T$ is $ω$ -consistent in the sense that it is not the case that for any $θ$ , $T ⊢ θ (cterm (n))^{i}$ for all $n \in ℕ$ and $T ⊢ {\forall x \neg θ (x)}^{i}$ . Then there is some $G$ such that $T ⊬ G^{i}$ and $T ⊬ \neg G^{i}$ .

Proof.

Gödel-number the expressions of $T$ as usual. As the set of theorems of $T$ is r.e. there is a $Δ_{0}$ formula $θ (x, y)$ such that for each $τ$ , we have that $ℕ ⊨ \exists x {Proof}_{T} (x, ⌜τ⌝)$ holds if and only if $T ⊢ τ$ . As the interpretation $i$ is recursive there is a $Δ_{0}$ formula $θ (x, y, z)$ such that for all $σ$ of the language of $S$ , $DOR ⊢ \exists z θ (⌜σ⌝, ⌜σ^{i}⌝, z)$ and $DOR ⊢ \neg \exists z θ (⌜σ⌝, k, z)$ for all other $k \in ℕ$ . Now let $G$ be such that

DOR ⊢ G \leftrightarrow \forall x \forall y \forall z (θ (⌜σ⌝, y, z) \to \neg {Proof}_{T} (x, y))

Apply the Gödel argument to show that $T ⊬ G^{i}$ and $T ⊬ \neg G^{i}$ .

The second theorem is slightly more complicated. We suppose that there is a provability predicate for $T$ in $S$ which is, there is an expression $Prov (⌜σ⌝)$ of the language of $S$ such that the following hold for each $σ, τ$ in the language of $S$ .

if $T ⊢ σ^{i}$ then $S ⊢ Prov (⌜σ^{i}⌝)$ ;
$S ⊢ Prov (⌜(σ \to τ)^{i}⌝) \to (Prov (⌜σ^{i}⌝) \to Prov (⌜τ^{i}⌝))$ ;
$S ⊢ Prov (⌜σ^{i}⌝) \to Prov (⌜Prov (⌜σ^{i}⌝)^{i}⌝)$ .

The statement of $S$ expressing the consistency of $T$ , or $Con (T)$ , is the expression of $S$ , $\neg Prov (⌜⊥^{i}⌝)$ , and this can of course be interpreted in $T$ .

Theorem.

Suppose that the set $\{τ: T ⊢ τ\}$ of theorems of $T$ is r.e., that $i : S ⟿ T$ is a recursive intepretation of a first order theory $S$ extending $DOR$ , and that $Prov$ is a provability predicate as above. Suppose $T$ is consistent in the sense that $T ⊬ ⊥^{i}$ Then $T ⊬ Con (T)^{i}$ .

Proof.

Similar to that given before in the page on Gödel's second incompleteness theorem. The main steps are sketched here.

First let $G$ be the statement of $S$ such that

S ⊢ G \leftrightarrow \neg Prov (⌜G^{i}⌝)

Then it can be shown that $T ⊢ G^{i}$ implies $T ⊢ ⊥^{i}$ .

Next let $σ$ be the statement of $S$ stating $G \to (Prov (⌜G^{i}⌝) \to ⊥)$ . Then applying the other rules for provability predicate and provability in $T$ and $S$ we find that $S ⊢ σ$ , hence $T ⊢ σ^{i}$ and $S ⊢ \neg Prov (⌜⊥^{i}⌝) \to \neg Prov (⌜G^{i}⌝)$ . It follows that if $T ⊢ (\neg Prov (⌜⊥^{i}⌝))^{i}$ then $T ⊢ (\neg Prov (⌜G^{i}⌝))^{i}$ and hence $T ⊢ G^{i}$ contradicting the previous part.

3. A simple kind of interpretation

In most casess we will be interpreting arithmetic, such as $DOR$ or some other theory in the same lanuguage in another first order theory $T$ . The most natural way to do this is to specify (in that theory $T$ ) the domain of the model of arithmetic and the definitions of addition and multiplication. These will be sets definable in the language of $T$ . Usually the domain is a definable set $D$ of $k$ -tuples for some $k$ modulo a definable equivalence relation (which needs to be shown to be, provably in $T$ , an equivalence relation on $D$ ). Then the definition of addition and multiplication have to be shown (in $T$ ) to be well-defined of course. This is the usual kind of interpretation of one theory in another. The reader will have to check that such definitions do indeed lead to a translation of formulas of one language into the other. (This isn't quite a triviality. It is not completely easy to see what to do about terms in the language of arithmetic, which you are trying to interpret in some purely relational language.)

In many cases, the equivalence relation can be omitted and all we need is the domain $D$ which might if we are lucky to be defined by a single formula $δ (x)$ is a single free variable. This will be the case in the main examples we will need: where some theory of sets interprets arithmetic, such as $PA$ or $DOR$ .