Home  Online Resources  Table of Contents

Journal of Logic and Computation, Volume 11, Issue 5, pp. 671-689: Abstract.

Internalization: The Case of Hybrid Logics

Jeremy Seligman

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

  Full-Text PDF  (203 KB)


[ Oxford University Press]   [ Oxford Journals]   [ Comments & Feedback]   Copyright© Oxford University Press, 2001.