Internalizing labelled deduction

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review


This paper shows how to internalize the Kripke satisfaction definition using the basic hybrid language, and explores the proof theoretic consequences of doing so. The basic hybrid language enables the transfer of classic Gabbay-style labelled deduction methods from the metalanguage to the object language, and the logical handling of labelling discipline. This internalized approach to labelled deduction links neatly with the Gabbay-style rules now widely used in modal Hilbert-systems, enables completeness results for a wide range of first-order definable frame classes to be obtained automatically, and extends to many richer languages. The paper discusses related work by Jerry Seligman and Miroslava Tzakova and concludes with some reflections on the status of labelling in modal logic.
TidsskriftJournal of Logic and Computation
Udgave nummer1
Sider (fra-til)137-168
Antal sider32
StatusUdgivet - feb. 2000
Udgivet eksterntJa

Citer dette