What is the definition of interpretability? Let $L_1$ and $L_2$ be first-order languages. Let $T_1$ and $T_2$ be theories over $L_1$ and $L_2$, respectively. What does it mean when one says that $T_2$ interprets $T_1$? I think this page explains the concept I'm mentioning, but it only has informal definition.
 A: Suppose we have a function $\Gamma$ that sends $L_1$-formulas to $L_2$-formulas, in such a way that the logical structure is preserved. So for example $\Gamma(\varphi\wedge \psi) = \Gamma(\varphi) \wedge \Gamma(\psi)$. Such a function is completely determined by where the atomic formulas are sent. Note that in all this we usually identify two formulas if they are equivalent modulo the relevant theory.
Such a function $\Gamma$ is said to be an interpretation of $T_1$ in $T_2$, also denoted as $\Gamma: T_1 \to T_2$, if for every axiom $\varphi\in T_1$ we have $T_2 \models \Gamma(\varphi)$.
I think the name really makes sense if you look at this from the perspective of models of the theories. Suppose we have a model $M$ of $T_2$, then we can make $M$ into an $L_1$-structure by interpreting relation symbols $R \in L_1$ as $\Gamma(R)$ and for function symbols $f \in L_1$ we consider the formula $\Gamma(f(x) = y)$, which defines the graph of a function (and hence a function) on $M$. Call this $L_1$-structure $\Gamma^*(M)$, then it should be clear that $\Gamma^*(M) \models \varphi(a)$ if and only if $M \models \Gamma(\varphi)(a)$ for every $L_1$-formula $\varphi$ and all $a \in M$. So since $M$ was a model of $T_2$ and $T_2 \models \Gamma(\varphi)$ for every $\varphi\in T_1$ we have that $\Gamma^*(M)$ is a model of $T_1$. So an interpretation $\Gamma: T_1 \to T_2$ gives us a way to interpret models of $T_2$ as models of $T_1$.
Edit: see also Andreas' comment about a possible extension of the definition in this answer, which allows you to restrict $\Gamma^*(M)$ to a definable subset of $M$.
