Internalizing labelled deduction

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.