How to identify, translate and combine logics?
Florian Rabe · Journal of Logic and Computation · 2014
We give general definitions of logical frameworks and logics. Examples include the logical frameworks LF and Isabelle and the logics represented in them. We apply this to give general definitions for equivalence of logics, translation between logics and combination of logics. We also establish general criteria for the soundness and completeness of these. Our key messages are that the syntax and proof systems of logics are theories; that both semantics and translations are theory morphisms; and that combinations are colimits. Our approach is based on the Mmt language, which lets us combine formalist declarative representations (and thus the associated tool support) with abstract categorical conceptualizations.