KD45

Overview

KD45 is one of the 15 distinct normal propositional systems of the Modal Logic Cube. It extends K with the axiom schema(s) D45. This is a familiar idealised belief logic: accessibility is serial, transitive, and Euclidean but need not be reflexive.

Language and Proof Theory

Formulas are generated from propositional atoms, Boolean connectives, and the unary operators \Box and \Diamond. Every system contains classical propositional tautologies and the normality axiom

\Box(\varphi\to\psi)\to(\Box\varphi\to\Box\psi).

The rules are modus ponens, uniform substitution, and necessitation (from a theorem \varphi, infer \Box\varphi). Additional characteristic axioms are:

• D (serial): \Box\varphi\to\Diamond\varphi; \forall x\,\exists y\,Rxy.
• 4 (transitive): \Box\varphi\to\Box\Box\varphi; \forall x\forall y\forall z\,((Rxy\land Ryz)\to Rxz).
• 5 (Euclidean): \Diamond\varphi\to\Box\Diamond\varphi; \forall x\forall y\forall z\,((Rxy\land Rxz)\to Ryz).

Kripke Semantics and Correspondence

The usual Kripke clauses apply: M,w\models\Box\varphi iff every R-successor of w satisfies \varphi. The relevant frame class consists of serial and transitive and Euclidean accessibility relations.

All these frame conditions are first-order properties of R, and the specified Hilbert logic is sound and complete for its corresponding frame class. Frame correspondence concerns validity on every valuation, not the truth of a modal formula at one particular valuation.

Worked Observation

An agent may consistently believe p when p is actually false, so T is not a theorem.

Decision Problems and Complexity

Local satisfiability is NP-complete, and the system has the finite model property. Validity is the complementary decision problem and has the corresponding coNP-complete bound in the NP cases, or PSPACE-completeness in the PSPACE cases. The modal cube is propositional and monomodal. The stated complexity is for local satisfiability in the ordinary language with freely many propositional atoms; quantified, multimodal and higher-order extensions may have different bounds.

Position in the Cube

• Immediate weaker systems: KD4, KD5, K45.
• Immediate stronger systems: S5.

References

1. Christoph Benzmüller, Maximilian Claus, and Nik Sultana (2015). Systematic Verification of the Modal Logic Cube in Isabelle/HOL. PxTP 2015, EPTCS 186, 27–41. arXiv.
2. Cláudia Nalon, Ullrich Hustadt, Fabio Papacchini, and Clare Dixon (2022). Local Reductions for the Modal Cube. IJCAR 2022. DOI.
3. Richard E. Ladner (1977). The Computational Complexity of Provability in Systems of Modal Propositional Logic. SIAM J. Comput. 6(3), 467–480. DOI.
4. Patrick Blackburn, Maarten de Rijke, and Yde Venema (2001). Modal Logic. Cambridge University Press.