Transfer between different signatures of the same logic I'm formalising parts of modal, intuitionistic and classical logic in Coq. So I have to keep track of nitty-gritty details.

*

*To simplify proofs that use the syntax, I'd like to use the signature $\langle \to, \bot \rangle$ for classical logic and $\langle \to, \Box, \bot\rangle$ for modal logic.

*For intuitionistic logic (and substructural logics) it is necessary to add the lattice operations to the signature. I.e. to work over $\langle \land, \lor, \to, \bot\rangle$.

*On the other hand, for boolean algebras as bounded distributive lattices with complement it is natural to write their signature as $\langle \land, \lor, \neg, \top, \bot\rangle$.

*For deduction systems it is often natural to choose the signature in a way, that all operations that are mentioned in inference rules or axioms are in the signature.

*A fragment of a logic only appears syntactically as a fragment, if the signatures are chosen appropriately. If I were to define classical logic via the signature $⟨\to, \bot⟩$ then it is syntactically "unnatural" to talk about its fragment $⟨\land, \lor, \top, \bot⟩$.

This is my motivation why I want to look at the same logic multiple times over different signatures.
Now given some semantics, deduction system or algorithm for a logic defined over some signature, which I want to "transfer" to the same logic defined over another language.
Are there efficient ways to formulate this situation and to shortcut for example correctness/completeness proofs of the transferred semantics etc.? Or to transfer proofs of commutativity/associativity of the operations?
Is there literature about this? I have "Abstract Algebraic Logic" by J.M.Font available, but did not find what I was looking for.
 A: I propose the following notion as a solution to my question.
Let $\mathcal{L}_0, \mathcal{L}_1$ be languages (i.e. sets of formulas over some possibly different signatures).
Let $=_0, =_1$ be equivalence relations on $\mathcal{L}_0$ and $\mathcal{L}_1$ respectively. Interpret $x_0 =_0 x_1$ as “the formulas $x_0$ and $x_1$ are equivalent in the logic under consideration”.
Two maps $f : \mathcal{L}_0 \to \mathcal{L}_1$, $g : \mathcal{L}_1 \to \mathcal{L}_0$ form an “adequate translation” between the two signatures/languages if the following conditions hold:

*

*$x=_0 g(f(x))$ for all $x \in \mathcal{L}_0$,

*$y=_1 g(f(y))$ for all $y \in \mathcal{L}_1$,

*for all $x_0, x_1 \in \mathcal{L}_0$, we have $x_0 =_0 x_1$ iff $f(x_0) =_1 f(x_1)$,

*for all $y_0, y_1 \in \mathcal{L}_1$, we have $y_0 =_1 y_1$ iff $g(y_0) =_0 g(y_1)$.

In other words, $f, g$ need to be inverses up to equivalence, and both need to preserve and reflect the equivalence relations.
This is similar to Def. 3.11 in “Abstract Algebraic Logic” by J.M.Font.
I did not verify (yet) whether such a translation provides the transfer principles which I was looking for. But it looks plausible. Further conditions like "$f$ and $g$ commute with substitutions" might be necessary as well. The same approach will probably work in a universal algebra situation.
