K

Overview

K is one of the 15 distinct normal propositional systems of the Modal Logic Cube. It is the minimal normal modal logic. No accessibility condition is imposed; dead-end worlds are permitted and make every box formula vacuously true.

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:

• No additional axioms beyond normal modal logic K.

Kripke Semantics and Correspondence

A Kripke frame F=(W,R) has nonempty W and arbitrary R\subseteq W\times W. A model M=(W,R,V) interprets box by

M,w\models\Box\varphi\iff\forall v\,(Rwv\to M,v\models\varphi).

Possibility is the dual \Diamond\varphi:=\neg\Box\neg\varphi.

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

The formula \Diamond p\land\Diamond\neg p requires two distinct successors of the evaluation world.

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: none.
• Immediate stronger systems: KD, KB, K4, K5.

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.