  We shall use a precise formal regimentation of this informal notion. Let T1 and T2 be recursively enumerable axiom systems.  We say that T1 is interpretable in T2 (T1 ≤ T2) when, roughly speaking, there is a translation τ from the language of T1 to the language of T2 such that, for each sentence φ of the language of T1, if T1⊢φ then  T2⊢τ(φ).[7] We shall write T1 &lt; T2 when T1≤ T2 and T2≰ T1 and we shall write T1≡ T2 when both T1≤ T2 and T2≤ T1.  In the latter case, T1 and T2 are said to be mutually interpretable.  The equivalence class of all theories mutually interpretable with T is called the interpretability degree of T.