From Hilbert Axioms to Frame Properties in Modal Logics

In the 1990s Dov Gabbay and myself developed an algorithmic method for eliminating existentially quantified predicates from second-order predicate logic formulae. We used it to automatically map Hilbert axioms of normal proposi- tional modal logics to the corresponding properties of the accessibility relation in its possible worlds semantics. “And what about completeness? ” was a ques- tion Dov kept asking. In this note I shortly present the method and put the finger on the points where the still unsatisfactorily solved completeness issues arise. 1 Two Ways for Characterizing Normal Propositional Modal Logics The formulae of propositional modal logic are like the formulae of standard propositional logic extended with the modal operators 2 (necessarily) and 3 (possibly). Their semantics can be characterized in different ways. Hilbert Calculus Kurt Gödel introduced the now traditional way for characterizing a modal logic by means of axioms and inference rules. The calculus for the basic normal propositional modal logic K consists of - the axioms for standard propositional logic, - the axiom K: 2(A → B) → (2A → 2B), - the Modus Ponens inference rule: From P and P → Q infer Q, - and the Necessitation Rule: If P is a theorem then 2P can be inferred. In principle one can add arbitrarily additional axioms, as long as the calculus remains consistent. Well known axioms are:

Authors

• Hans Jürgen Ohlbach

Keywords

No keywords are indexed for this paper.