Maybe the best known example is the interpretation of Peano arithmetic into ZFC. Peano arithmetic has a language with a constant symbol $0$ and a unary function symbol $S$. The language of ZFC has neither of these. But we can interpret Peano arithmetic into ZFC as follows:
- $0$ is interpreted as the empty set $\emptyset$
- Every variable is interpreted as itself
- Logical connectives are interpreted as themselves
- $S(t)$, where $t$ is a term, is interpreted as $t' \cup \{t'\}$, where $t'$ is the interpretation of $t$.
- The number quantifiers $(\forall n)$ and $(\exists n)$ are replaced with $(\forall x \in \omega)$ and $(\exists x \in \omega)$, respectively.
These rules allow every formula $\phi$ of PA to be replaced by a formula $\phi'$ of ZFC. For example the formula $(\exists m)(n = S(m))$ becomes $(\exists m \in \omega)(n = m \cup \{m\})$. Similarly, the induction axiom $ (0 \in X) \land (\forall m)[m \in X \to S(m) \in X] \to (\forall m)[m \in X] $ becomes $ (\emptyset \in X) \land (\forall m \in \omega)[m \in X \to m \cup \{m\} \in X] \to (\forall m \in \omega)[m \in X]. $
This interpretation is sound: if $\phi$ is a formula in the language of arithmetic that is provable in PA, the corresponding formula $\phi'$ is provable in ZFC.
One role of interpretations is to prove relative consistency results. Because of the fact in the previous sentence, if a contradiction $\psi$ is provable in PA then a different contradiction $\psi'$ is provable in ZFC. Thus if ZFC is consistent, so it proves no contradictions, then the soundness of the interpretation means that PA is a also consistent.
Other examples of interpretations include:
The interpretation of the (theory of the) field of complex numbers into the (theory of the) field of real numbers, where each complex number is represented by a pair of real numbers and the operations on complex numbers are defined appropriately in terms of the components.
Interpretations of non-Euclidean geometry into Euclidean geometry, for example by interpreting "lines" as great circles on a sphere.
The interpretation of Euclidean geometry into the field of real numbers, where each "point" is a pair of real numbers and each "line" is a pair of points, with an appropriate equivalence relation on the lines. This gives a relative consistency proof of Euclidean geometry.