© 2001 by Oxford University Press
| ||||||||||||||||||||||||||||||||||||||||||||||||||
Internalization: The Case of Hybrid Logics
1 Department of Philosophy, The University of Auckland, Private Bag 92019, Auckland, New Zealand. E-mail: j.seligman@auckland.ac.nz
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
![]()
CiteULike
Connotea
Del.icio.us What's this?
This article has been cited by other articles:
![]() |
T. Bolander and T. Brauner Tableau-based Decision Procedures for Hybrid Logic J Logic Computation, December 1, 2006; 16(6): 737 - 763. [Abstract] [Full Text] [PDF] |
||||
