Pure extensions, proof rules, and hybrid axiomatics (Q863181)

Hybrid modal (formal) languages are modal (formal) languages having the expressive power to name possible worlds, asserting equalities between worlds, and describing accessibility relations. In this paper, the authors examine three different kinds of hybrid languages for propositional modal logic and one kind of hybrid language for first-order quantified modal logic; they also characterize semantic systems for all of these kinds of languages. These systems are possible worlds semantics in the fashion of Kripke's semantics, with additional clauses accommodating the syntactic peculiarities of the hybrid languages considered. For each kind of hybrid modal languages, axiomatic formal systems are presented by the authors. Some of these systems contain, among others, certain non-orthodox proof rules; these rules are widely discussed in the paper. Strong completeness theorems are proved for the two axiomatic systems formulated for the most expressive sort of the hybrid propositional logic languages (considered by the authors). For the other axiomatic systems, strong completeness theorems are rather proved for extensions of the systems by means of certain kinds of rules and/or axioms with respect to models satisfying the frame properties defined by those same rules and/or axioms. The completeness proofs are Henkin proofs and differ, in this way, from the standard modal approach by means of canonical models. It is important to point out that, as a result of the expressive power of the hybrid languages, the completeness results cover frame classes that are not definable in orthodox modal languages.