Internalization: The Case of Hybrid Logics
Jeremy Seligman · Journal of Logic and Computation · 2001
A sequent calculus for hybrid logics is developed from a calculus for classical predicate logic by a series of transformations. We formalize the semantic theory of hybrid logic using a sequent calculus for predicate logic plus axioms. This works, but it is ugly. The unattractive features are removed one‐by‐one, until the final vestiges of the metalanguage can be set aside to reveal a fully internalized calculus. The techniques are quite general and can be applied to a wide range of hybrid and modal logics.