Overview
KT is one of the 15 distinct normal propositional systems of the Modal Logic Cube. It extends K with the axiom schema(s) T. Reflexivity entails seriality, so D holds already, but symmetry and transitivity need not hold.
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:
- T (reflexive): \Box\varphi\to\varphi; \forall x\,Rxx.
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 reflexive 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
From \Box p one may infer p at the current 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
References
- 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.
- Cláudia Nalon, Ullrich Hustadt, Fabio Papacchini, and Clare Dixon (2022). Local Reductions for the Modal Cube. IJCAR 2022. DOI.
- Richard E. Ladner (1977). The Computational Complexity of Provability in Systems of Modal Propositional Logic. SIAM J. Comput. 6(3), 467–480. DOI.
- Patrick Blackburn, Maarten de Rijke, and Yde Venema (2001). Modal Logic. Cambridge University Press.