Internalizing labelled deduction

Publikation: Bidrag til tidsskriftTidsskriftartikelpeer review

Abstract

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.
OriginalsprogEngelsk
TidsskriftJournal of Logic and Computation
Vol/bind10
Udgave nummer1
Sider (fra-til)137-168
Antal sider32
ISSN0955-792X
DOI
StatusUdgivet - feb. 2000
Udgivet eksterntJa

Citer dette