Journal of Logic and Computation, Volume 11, Issue 5, pp. 671-689: Abstract.
Internalization: The Case of Hybrid Logics
Department of Philosophy, The University of Auckland, Private Bag 92019, Auckland, New Zealand. E-mail: email@example.com
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.
Keywords: Proof theory, cut-, elimination, internalization, hybrid logic, modal logic, subformula property, sequent calculus