What is the formal definition of a translation between theories? I've heard the expression "a translation from theory $A$ to theory $B$" thrown around a bit, but never encountered a formal definition. What is a translation between first-order theories? Furthermore, does this make the class of all theories over a signature into a category, where the morphisms are translations?

This is one of those cases where the devil is in the details, and there is a variety of notions hereabouts of different strengths. Can I suggest two resources, both freely available online?

Giorgi Japaridze and Dick de Jongh's contribution to the _Handbook of Proof Theory_ deals with 'Notions of interpretability' in their §11, starting at p. 500: <

For category theoretic considerations, see Albert Visser's 'Categories of theories and interpretations' available at <