Interpretations Between Theories

Two theories can be compared by the models they share or by a translation carrying one inside the other. When every sentence of $T_0$ renders as a sentence of $T_1$ so that theorems map to theorems, $T_1$ is at least as strong as $T_0$, even across different languages. The mechanism is an interpretation, and its simplest instance is the introduction of a defined symbol.

Defined function symbols

A definition differs from an axiom: it is declared by fiat rather than proved, so adding a defined symbol should not let one prove new statements in the old vocabulary. A careless definition violates this. Introducing a one-place symbol $f$ into number theory by

names $f(1)$ ambiguously: both $1<2$ and $1<3$, so $f(1)=2$ and $f(1)=3$, whence $2=3$. The failure is that the defining condition does not single out a unique value.

Consider a theory $T$ in a language without the one-place function symbol $f$, and add $f$ by the sentence

where $\phi$ is a formula of the original language with only $v_1,v_2$ free. Two conditions on this definition coincide.

A definition that meets the uniqueness condition adds nothing to the old theory's stock of theorems.¹ This is the prototype of a translation between languages: the augmented theory $\text{Cn }(T;\delta )$ sits atop $T$, and $T$ is already as strong.

Interpretations

The general situation replaces the identity translation of a defined symbol with an arbitrary assignment of formulas to the vocabulary of another language. To avoid symbol clashes, the two languages $L_0$ and $L_1$ are taken as reducts of a common parent.

The domain formula carves out, inside any model of $T_1$, the set that will serve as the universe of a translated $L_0$-structure. Each predicate becomes a definable relation restricted to that domain; each function symbol becomes a definable graph that the interpretation requires to be a genuine total function.

Arithmetic inside the integers

The standard example interprets the theory of $(\mathbb{N};0,S)$ into the theory of $(\mathbb{Z};+,\cdot )$. The first ingredient is Lagrange's four-square theorem: an integer is nonnegative exactly when it is a sum of four squares. This makes $\mathbb{N}$ a definable subset of $\mathbb{Z}$, so it can serve as the domain formula. The zero and successor symbols are then definable in $(\mathbb{Z};+,\cdot )$ as well:

The domain formula picks out the nonnegative integers; ${\pi }_0$ isolates $0$ as the unique idempotent of addition; ${\pi }_S$ defines the successor relation by adding the multiplicative idempotent $z=1$ distinct from $0$.

The identity interpretation, where ${\pi }_{\forall }=(v_1=v_1)$ and each symbol maps to itself, exists trivially for any $T_1$ and recovers the case of a defined symbol: $\pi$ is the identity on all symbols except $f$, and ${\pi }_f=\phi$.²

From models to structures

An interpretation lets any model of $T_1$ generate an $L_0$-structure. Given $\mathfrak{B}\models T_1$, define $\pi \mathfrak{B}$ with universe the set defined by ${\pi }_{\forall }$, each predicate the relation defined by ${\pi }_P$ restricted to that universe, and each function the map whose graph ${\pi }_f$ defines. The nonemptiness and totality conditions in the definition are exactly what make $\pi \mathfrak{B}$ a well-formed structure. Collecting the sentences true in all such structures gives a theory:

This is satisfiable iff $T_1$ is. In the defined-symbol case it recovers $\text{Cn }(T;\delta )$: every model of $T;\delta$ is $\pi \mathfrak{A}$ for its restriction $\mathfrak{A}$ to the smaller language.

Syntactic translation

Beyond the model-theoretic picture, the interpretation acts directly on formulas. Each $L_0$-formula $\phi$ has a translation ${\phi }^{\pi }$ in $L_1$, defined by recursion. For a nonatomic formula the translation commutes with the connectives and relativizes quantifiers to the domain:

The quantifier clause is the essential case: a claim for all $x$ in the source becomes for all $x$ in the domain in the target, guarding the universal with the domain formula so that quantifiers range only over the translated universe.

For atomic formulas the translation must undo nested function symbols, since a target-language predicate takes only variables through its defining formula. Scanning an atomic formula from right to left, each innermost function term $g{x}_1\cdots x_n$ is replaced by a fresh variable $y$ prefixed with $\forall y({\pi }_g(x_1,\dots ,x_n,y)\to \cdots )$, until only a predicate applied to variables remains.

The translation is designed so that satisfaction is preserved in both directions.

The lemma is not deep; it records that ${\phi }^{\pi }$ was defined correctly, and its proof is an induction whose only nontrivial case is an atomic formula with nested functions. Specializing to sentences gives the reason for the notation ${\pi }^{-1}[T_1]$.³

Faithful interpretations and transfer

An interpretation of a theory requires that theorems map to theorems.

The largest theory $\pi$ interprets into $T_1$ is ${\pi }^{-1}[T_1]$; faithfulness is the case of equality, where the translation reflects nonmembership as well as membership.

The arithmetic example is faithful: $\pi (\mathbb{Z};+,\cdot )$ is exactly $(\mathbb{N};0,S)$, so

There is no interpretation the other way — $\text{Th }(\mathbb{Z};+,\cdot )$ cannot be interpreted into $\text{Th }(\mathbb{N};0,S)$ — so the theory of integer arithmetic is strictly stronger, a fact established through definability in arithmetic. For defined symbols, faithfulness yields eliminability.

Every use of the defined symbol can be replaced by a provably equivalent sentence in the original vocabulary.

Transporting decidability

A faithful interpretation moves decision problems between theories. If $\pi$ faithfully interprets $T_0$ into $T_1$ and $T_1$ is decidable, then $T_0$ is decidable: to test $\sigma \in T_0$, compute ${\sigma }^{\pi }$ and test ${\sigma }^{\pi }\in T_1$. Run backward, the same link transports undecidability: if $T_0$ is undecidable and interprets into $T_1$, then $T_1$ is undecidable too, since a decision procedure for $T_1$ would yield one for $T_0$. This backward transfer is the standard route by which the undecidability of number theory spreads to set theory and beyond, developed through the incompleteness theorems.