(This started as an answer on Math.Stackexchange. This version has been lightly edited and expanded. Also posted at fff.)
Throughout this post, theory means first-order theory. In fact, we are concerned with theories that are recursively presented, though the abstract framework applies more generally. Thanks to Fredrik Engström Ellborg for suggesting in Google+ the reference Kaye-Wong, and to Ali Enayat for additional references and many useful conversations on this topic.
1.
Informally, to say that a theory interprets a theory
means that there is a procedure for associating structures
in the language of
to structures
in the language of
in such a way that if
is a model of
, then
is a model of
.
Let us be a bit more precise, and do this syntactically to reduce the requirements of the metatheory. The original notion is due to Tarski, see
Alfred Tarski. Undecidable theories. In collaboration with Andrzej Mostowski and Raphael M. Robinson. Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Company, Amsterdam, 1953. MR0058532 (15,384h).
I follow here the modern reference on interpretations,
Albert Visser, Categories of theories and interpretations, in Logic in Tehran, Lecture Notes in Logic, vol. 26, Association for Symbolic Logic, La Jolla, CA, 2006, pp. 284–341. MR2262326 (2007j:03083).
One can take “the theory interprets the theory
” to mean that there are
- A map
that assigns formulas in the language of
to the symbols of the language
of
, and
- A formula
in the language of
,
with the following properties: We can extend to all
-formulas recursively:
, etc, and
. It then holds that
proves
, and
for each axiom
of
(including the axioms of first-order logic).
Here, are taken to be recursive, and so is
.
If the above happens, then we can see as a strong witness to the fact that the consistency of
implies the consistency of
.
Two theories are mutually interpretable iff each one interprets the other. By the above, this is a strong version of the statement that they are equiconsistent.
Two theories are bi-interpretable iff they are mutually interpretable, and in fact, the interpretations from
is
and
from
in
can be taken to be “inverses” of each other, in the sense that
proves that
and
are equivalent for each
in the language of
, and similarly for
,
and
. In a sense, two theories that are bi-interpretable are very much “the same”, only differing in their presentation.