K4

Overview

K4 is one of the 15 distinct normal propositional systems of the Modal Logic Cube. It extends K with the axiom schema(s) 4. Transitivity does not imply reflexivity or seriality; finite strict orders provide examples.

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:

• 4 (transitive): \Box\varphi\to\Box\Box\varphi; \forall x\forall y\forall z\,((Rxy\land Ryz)\to Rxz).

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 transitive 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

If \Box p holds at w, then \Box\Box p holds there as well.

Decision Problems and Complexity

Local satisfiability is PSPACE-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: K.
• Immediate stronger systems: KD4, K45.

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.