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.