---
title: Interpretations Between Theories
module: Models, Compactness, and Theories
moduleNumber: 5
lessonNumber: 3
order: 503
summary: >
  An interpretation translates the vocabulary of one theory into formulas of
  another, relativizing quantifiers to a definable domain and mapping symbols to
  defining formulas. Defined function symbols meet a noncreativity criterion;
  the syntactic translation of formulas carries theoremhood forward, and a
  faithful interpretation transfers decidability and undecidability between
  theories.
topics: [Models, Compactness, and Theories]
sources:
  - book: Enderton
    ref: "Ch. 2 — First-Order Logic; §2.7 Interpretations Between Theories"
draft: false
---

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

$$
f(x) = y \quad \text{iff} \quad x < y
$$

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.

> **Worked example (A creative definition and the uniqueness it violates).**
> Introduce $f$ into number theory by
> $$
> \delta : \forall v_1 \, \forall v_2 \,(f v_1 = v_2 \leftrightarrow v_1 < v_2).
> $$
> The associated well-definedness sentence is
> $\varepsilon : \forall v_1 \, \exists! v_2 \,(v_1 < v_2)$, which fails in
> $\fN$: every number has infinitely many numbers above it, not exactly one.
> So $\varepsilon \notin \Th \fN$, and by the noncreativity criterion below the
> definition is creative. The damage is explicit: $1 < 2$ forces $f1 = 2$ and
> $1 < 3$ forces $f1 = 3$, so
> $$
> 2 = f1 = 3,
> $$
> a sentence of the original language derivable from $T; \delta$ but false in
> $\fN$. The definition manufactures a new theorem, and noncreativity forbids
> precisely that.

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

$$
(\delta) \qquad \forall v_1 \, \forall v_2 \, [\, f v_1 = v_2 \leftrightarrow \varphi \,],
$$

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

> **Theorem (Noncreativity and well-definedness of definitions).** The following are equivalent.
> (a) The definition is _noncreative_: for any sentence $\sigma$ of the smaller
> language, $T; \delta \models \sigma$ implies $T \models \sigma$.
> (b) $f$ is _well defined_: the sentence
> $(\varepsilon) \; \forall v_1 \, \exists! v_2 \, \varphi$ belongs to $T$.

> **Proof.** For (a) $\Rightarrow$ (b): $\delta \models \varepsilon$, so taking
> $\sigma = \varepsilon$ in noncreativity gives $T \models \varepsilon$. For the
> converse, let $\fA$ be a model of $T$. Since $T \models \varepsilon$,
> for each $d$ there is a unique $e$ with $\fA \models \varphi[d, e]$;
> define $F(d) = e$. The expansion $(\fA, F)$ interpreting $f$ by $F$
> models $\delta$ and satisfies the same original-language sentences as
> $\fA$. So $T; \delta \models \sigma$ forces $\sigma$ true in
> $(\fA, F)$, hence in $\fA$. $\square$

A definition that meets the uniqueness condition adds nothing to the old
theory's stock of theorems.[^def] This is the prototype of a translation between
languages: the augmented theory $\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.

> **Definition (Interpretation).** An interpretation $\pi$ of a language $L_0$
> into a theory $T_1$ (in language $L_1$ with equality) assigns:
> - to $\forall$ a **domain formula** $\pi_\forall$ with at most $v_1$ free,
>   satisfying $T_1 \models \exists v_1 \, \pi_\forall$ (the domain is nonempty);
> - to each $n$-place predicate $P$ a formula $\pi_P$ with at most
>   $v_1, \dots, v_n$ free;
> - to each $n$-place function symbol $f$ a formula $\pi_f$ with at most
>   $v_1, \dots, v_{n+1}$ free, such that in every model of $T_1$, $\pi_f$
>   defines a total function on the domain into the domain.

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.

$$
% caption: An interpretation sends each symbol of the source language to a
% formula of the target theory: the universe symbol to a domain formula, and
% each relation and function symbol to a defining formula.
\begin{tikzpicture}[scale=1.0, >=stealth, font=\footnotesize]
  \definecolor{acc}{HTML}{4A6FA5}
  \node[align=center, font=\scriptsize] at (0,2.3) {symbols of source};
  \node[align=center, font=\scriptsize] at (6.2,2.3) {formulas of target theory};
  \node[draw, minimum width=26mm, minimum height=8mm] (u) at (0,1.4) {universe};
  \node[draw, minimum width=26mm, minimum height=8mm] (p) at (0,0.2) {predicate};
  \node[draw, minimum width=26mm, minimum height=8mm] (f) at (0,-1.0) {function};
  \node[draw=acc, thick, minimum width=32mm, minimum height=8mm] (du) at (6.2,1.4) {domain formula};
  \node[draw=acc, thick, minimum width=32mm, minimum height=8mm] (dp) at (6.2,0.2) {def\/ining relation};
  \node[draw=acc, thick, minimum width=32mm, minimum height=8mm] (df) at (6.2,-1.0) {def\/ining graph};
  \draw[->, acc, thick] (u) -- (du);
  \draw[->, acc, thick] (p) -- (dp);
  \draw[->, acc, thick] (f) -- (df);
\end{tikzpicture}
$$

### 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:

$$
\pi_\forall(x) = \exists y_1 \cdots \exists y_4 \; x = y_1 \cdot y_1 + y_2 \cdot y_2 + y_3 \cdot y_3 + y_4 \cdot y_4,
$$
$$
\pi_0(x) = (x + x = x),
\qquad
\pi_S(x, y) = \forall z \, (z \cdot z = z \wedge z + z \neq z \to x + z = y).
$$

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$.

$$
% caption: The four-square formula carves the nonnegative integers out of
% $\mathbb{Z}$, supplying the domain on which zero and successor are then
% definable.
\begin{tikzpicture}[scale=1.0, >=stealth, font=\footnotesize]
  \definecolor{acc}{HTML}{4A6FA5}
  \draw[thick] (-0.2,0) -- (8.0,0);
  \foreach \x in {0.6,1.6,2.6} \fill (\x,0) circle (1.6pt);
  \foreach \x in {3.2,3.4,3.6} \fill (\x,0) circle (0.8pt);
  \foreach \x in {4.2,5.2,6.2,7.2} \fill[acc] (\x,0) circle (1.9pt);
  \node[below, font=\scriptsize] at (2.0,-0.15) {negatives};
  \node[acc, below, font=\scriptsize] at (6.0,-0.15) {nonnegatives};
  \draw[acc, thick] (4.2,0.4) -- (4.2,0.6) -- (7.2,0.6) -- (7.2,0.4);
  \node[acc, font=\scriptsize, align=center] at (5.7,1.05) {sums of four squares\\= the domain};
\end{tikzpicture}
$$

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 =
\varphi$.[^interp]

## From models to structures

An interpretation lets any model of $T_1$ generate an $L_0$-structure. Given
$\fB \models T_1$, define $\pi\fB$ 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\fB$ a well-formed structure. Collecting the sentences
true in all such structures gives a theory:

$$
\pi^{-1}[T_1] = \Th\{\pi\fB \mid \fB \models T_1\}.
$$

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

## Syntactic translation

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

$$
(\neg\varphi)^\pi = \neg(\varphi^\pi),
\quad
(\varphi \to \psi)^\pi = (\varphi^\pi \to \psi^\pi),
\quad
(\forall x \, \varphi)^\pi = \forall x \, (\pi_\forall(x) \to \varphi^\pi).
$$

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.

$$
% caption: A source-language quantifier is relativized to the target domain: it
% ranges only over the elements the domain formula admits, not the whole
% universe of the interpreting model.
\begin{tikzpicture}[scale=1.0, >=stealth, font=\footnotesize]
  \definecolor{acc}{HTML}{4A6FA5}
  \draw[draw=black, fill=black!5] (0,0) ellipse (3.0 and 1.9);
  \node[font=\scriptsize] at (0,1.45) {interpreting model};
  \draw[draw=acc, thick, fill=acc!12] (0,-0.25) ellipse (1.7 and 0.95);
  \node[acc, align=center, font=\scriptsize] at (0,-0.25) {domain\\(where quantif\/iers range)};
\end{tikzpicture}
$$

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.

> **Worked example (Translating an atomic formula with nested functions).**
> The atomic formula $P f g x$ applies $P$ to the term $fgx$. Scan right to
> left. The innermost function term is $gx$; replace it by a fresh $y$ guarded
> by $\pi_g$. Next comes $f(\cdot)$; replace $fy$ by a fresh $z$ guarded by
> $\pi_f$. What remains is $Pz$, translated by $\pi_P$:
> $$
> \begin{aligned}
> (P f g x)^\pi &= \forall y \,\big(\pi_g(x, y) \to (P f y)^\pi\big) \\
>   &= \forall y \,\big(\pi_g(x, y) \to \forall z \,(\pi_f(y, z) \to (P z)^\pi)\big) \\
>   &= \forall y \,\big(\pi_g(x, y) \to \forall z \,(\pi_f(y, z) \to \pi_P(z))\big).
> \end{aligned}
> $$
> Each function symbol becomes a universally quantified fresh variable
> constrained by its defining graph, leaving target predicates applied to
> variables alone.

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

> **Lemma (Translation lemma for interpretations).** For an interpretation $\pi$ of $L_0$ into $T_1$, a model
> $\fB$ of $T_1$, a formula $\varphi$ of $L_0$, and an assignment $s$
> into the domain $|\pi\fB|$,
> $$
> \pi\fB \models \varphi[s] \quad\text{iff}\quad \fB \models \varphi^\pi[s].
> $$

The lemma is not deep; it records that $\varphi^\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]$.[^trans]

> **Corollary (Interpretations preserve theoremhood).** For a sentence $\sigma$ of $L_0$,
> $\sigma \in \pi^{-1}[T_1]$ iff $\sigma^\pi \in T_1$.

> **Worked example (Translating a sentence about successor into $(\mathbb{Z}; +, \cdot)$).**
> The sentence $\forall x \, Sx \neq 0$ of $(\mathbb{N}; 0, S)$ says no successor
> is zero. Under the interpretation $\pi$ it becomes a statement about integers.
> Relativize the quantifier to the domain formula, then unwind the atomic
> $Sx = 0$ through the defining formulas $\pi_0(u) = (u + u = u)$ and
> $\pi_S(x, v) = \forall z(z \cdot z = z \wedge z + z \neq z \to x + z = v)$:
> $$
> (\forall x \, Sx \neq 0)^\pi
>   = \forall x \Big[\pi_\forall(x) \to
>     \neg\,\forall u\big(u + u = u \to \forall v(\pi_S(x, v) \to v = u)\big)\Big],
> $$
> where $\pi_\forall(x) = \exists y_1 \exists y_2 \exists y_3 \exists y_4 \;
> x = y_1 y_1 + y_2 y_2 + y_3 y_3 + y_4 y_4$. The inner clause reads "the
> successor of $x$ is not the additive idempotent $0$," now written with $+$ and
> $\cdot$ alone. The result belongs to $\Th(\mathbb{Z}; +, \cdot)$, matching the
> truth of $\forall x \, Sx \neq 0$ in $(\mathbb{N}; 0, S)$.

## Faithful interpretations and transfer

An interpretation _of a theory_ requires that theorems map to theorems.

> **Definition (Interpretation of a theory).** An interpretation $\pi$ of $T_0$
> into $T_1$ is an interpretation of the language of $T_0$ into $T_1$ with
> $T_0 \subseteq \pi^{-1}[T_1]$; equivalently, $\sigma \in T_0$ implies
> $\sigma^\pi \in T_1$. It is **faithful** if $T_0 = \pi^{-1}[T_1]$, so that
> $\sigma \in T_0$ iff $\sigma^\pi \in T_1$.

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.

$$
% caption: Along an interpretation of theories, a theorem of the source becomes,
% after translation, a theorem of the target; a faithful interpretation reflects
% non-theorems as well.
\begin{tikzpicture}[scale=1.0, >=stealth, font=\footnotesize]
  \definecolor{acc}{HTML}{4A6FA5}
  \node[draw, minimum width=30mm, minimum height=9mm, align=center] (s) at (0,0.8) {theorem of source};
  \node[draw=acc, thick, minimum width=30mm, minimum height=9mm, align=center] (t) at (6.4,0.8) {theorem of target};
  \draw[->, acc, thick] (s) -- (t);
  \node[acc, font=\scriptsize] at (3.2,1.25) {translate};
  \node[draw, minimum width=30mm, minimum height=9mm, align=center] (s2) at (0,-1.0) {non-theorem of source};
  \node[draw, minimum width=30mm, minimum height=9mm, align=center] (t2) at (6.4,-1.0) {non-theorem of target};
  \draw[->, black, thick, dashed] (t2) -- (s2);
  \node[font=\scriptsize] at (3.2,-0.55) {ref\/lected only when faithful};
\end{tikzpicture}
$$

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

$$
(\mathbb{N};0,S) \models \sigma \;\Longleftrightarrow\; \pi(\mathbb{Z};+,\cdot) \models \sigma \;\Longleftrightarrow\; (\mathbb{Z};+,\cdot) \models \sigma^\pi.
$$

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

> **Theorem (Elimination of defined symbols).** In the defined-symbol situation, for any $L^+$-sentence
> $\sigma$ there is a sentence $\sigma^\pi$ in the original language with
> (a) $T; \delta \models (\sigma \leftrightarrow \sigma^\pi)$;
> (b) $T; \delta \models \sigma$ iff $T \models \sigma^\pi$;
> (c) if $f$ does not occur in $\sigma$, then $\models (\sigma \leftrightarrow \sigma^\pi)$.

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](/logic/incompleteness/incompleteness-and-undecidability).

| Direction | Given | Transferred |
| --- | --- | --- |
| forward | $T_1$ decidable, $\pi: T_0 \to T_1$ faithful | $T_0$ decidable |
| backward | $T_0$ undecidable, $\pi: T_0 \to T_1$ | $T_1$ undecidable |
| theorems | $\sigma \in T_0$ | $\sigma^\pi \in T_1$ |

[^def]: Enderton, §2.7 — defined function symbols, the noncreativity/well-definedness equivalence (Theorem 27A), and the eliminability of definitions (Theorem 27D).
[^interp]: Enderton, §2.7 — the definition of an interpretation, the arithmetic-in-integers example via Lagrange's theorem, and the extracted structure $\pi\fB$.
[^trans]: Enderton, §2.7 — the syntactic translation $\varphi^\pi$, Lemma 27B, Corollary 27C, and faithful interpretations.