What does it mean for two theories to be inter-interpretable? Mc Larty, is his article "Exploring Categorical Structuralism", gives a proof that the set theory ZFC is inter-interpretable with ETCS+R, a categorical version of set theory.
Intuitively, I get the idea. But is there any precise definition of inter-interpretability?
In terms of proof theory and model theory, what does it mean to say that two theories are inter-interpretable? 
In other words, what are the interesting consequences of inter-interpretability?
Can you give me a good reference to read more about those issues?
 A: An interpretation of one theory $T$ in another theory $S$ is essentially an appropriate tuple of formulas $\Phi$ (one formula for each symbol in the language of $S$, plus another formula for "domain") such that in any model $M$ of $T$, we have "$\Phi^T\models S$" - that is, $\Phi$ defines in $M$ a set and some relations/functions on that set which together form a model of $S$. 
For example, consider the usual construction of $\mathbb{C}$ as ordered pairs of reals. This corresponds to an interpretation of $Th(\mathbb{C};+,\cdot)$ in $Th(\mathbb{R};+,\cdot)$; the formulas in question are 


*

*$\varphi_{domain}(x,y)\equiv \top$ (the domain is all ordered pairs),

*$\varphi_+(x_1,x_2,y_1,y_2,z_1,z_2)\equiv (x_1+y_1=z_1)\wedge (x_2+y_2=z_2)$ (addition is componentwise), and

*$\varphi_\cdot(x_1,x_2,y_1,y_2,z_1,z_2)\equiv (x_1\cdot y_1-x_2\cdot y_2=z_1)\wedge(x_1\cdot y_2+x_2\cdot y_1=z_2)$ (multiplication treats the second coordinate like $i$ - note that I'm using subtraction here, which I shouldn't really, but since it's definable in terms of $+$ this is a benign abbreviation).
(A precise definition can be found in either of Hodges' model theory books, and this blog post of Hamkins - which I also cite below for a technical result - gives a good description of the notion.)
For a more technical example, forcing gives a method for constructing interpretations: e.g. the proof that ZFC+$\neg$CH is consistent if ZFC is ultimately amounts to constructing an interpretation $\Phi$ of ZFC+$\neg$CH in ZFC (with a bit of thought taken to handle non-well-founded models).

Two theories are then inter-interpretable (or mutually interpretable) if each is interpretable in the other. Interestingly there is a sharper version, called bi-interpretability, which requires that the interpretations commute nicely: given $M\models T$, we need "($M$'s model of $S$)'s model of $T$" to be isomorphic to $M$ (and similarly with $S$ and $T$ switched).
(In fact we require even more than that even: we need such isomorphisms to be uniformly definable. But this is a bit technical so I'll ignore it for now.)
This is in general a stronger condition than mere mutual interpretability; see e.g. here to see a stark difference.
