KB5

Overview

KB5 is one of the 15 distinct normal propositional systems of the Modal Logic Cube. It extends K with the axiom schema(s) B5. Over Kripke frames symmetry and Euclideanness together imply transitivity. Thus KB5 and KB4 define the same normal modal logic. Isolated worlds remain possible.

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:

• B (symmetric): \varphi\to\Box\Diamond\varphi; \forall x\forall y\,(Rxy\to Ryx).
• 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 symmetric 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

All connected non-isolated components behave as equivalence classes; an isolated world shows why S5 is strictly stronger.

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: KB, K45.
• Immediate stronger systems: S5.

Coincidence: \mathsf{KB5}=\mathsf{KB4} as logics; the latter uses B and 4 instead of B and 5. This does not identify KB5 with 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.