K Modal Logic

Origin. The distribution axiom appears in Gödel, "Eine Interpretation des intuitionistischen Aussagenkalküls" (1933), as one of three axioms for his provability calculus. Kripke, "A Completeness Theorem in Modal Logic" (1959) and "Semantical Analysis of Modal Logic I: Normal Modal Propositional Calculi" (1963), supplied the relational semantics and the completeness proof. Lemmon and Scott's notes, circulated from 1966 and published as An Introduction to Modal Logic (1977), fixed the practice of naming systems as K plus a list of axioms. K is the smallest normal modal logic: every normal system extends it.

Models. Kripke frames ⟨W, R⟩ with W a non-empty set of worlds and R an arbitrary binary relation — no reflexivity, transitivity or seriality is assumed. A model adds a valuation V: Prop → ℘(W). Dead ends, where w has no R-successors, are permitted and make □A vacuously true there. Algebraically the same logic is the equational theory of Boolean algebras with a single normal additive operator (Jónsson and Tarski, 1951).

Formalism.

Language: Propositional + □, ◇. □A: necessarily A. ◇A := ¬□¬A: possibly A.

Axioms: All propositional tautologies. K: □(A → B) → (□A → □B). Distribution axiom.

Rules: Modus ponens. Necessitation: from ⊢ A, infer ⊢ □A. Theorems are necessary.

Semantics: Frame F = ⟨W, R⟩. W: worlds. R: accessibility (arbitrary). No conditions on R.

Truth: M, w ⊨ □A iff for all v: wRv implies M, v ⊨ A. M, w ⊨ ◇A iff for some v: wRv and M, v ⊨ A.

What K lacks: Not □A → A (T). Not □A → □□A (4). Not ◇A → □◇A (5). Minimal assumptions.

Theorem examples: □(A ∧ B) ↔ □A ∧ □B. □A → ◇A invalid. ◇(A ∨ B) ↔ ◇A ∨ ◇B.

Normality: A logic is normal iff it contains K and is closed under necessitation, modus ponens and uniform substitution. K is the intersection of all normal modal logics.

Standard translation: ST_x(p) = Px. ST_x(¬A) = ¬ST_x(A). ST_x(□A) = ∀y (Rxy → ST_y(A)). Maps the modal language into first-order logic with one binary relation, using two variables.

Local vs global consequence: Γ ⊨_loc A: A true wherever all of Γ is true, same world. Γ ⊨_glob A: A globally true in every model where Γ is. Necessitation is sound for global, not local, consequence. The deduction theorem holds for local consequence only.

Extensions: KT: + reflexive. K4: + transitive. KB: + symmetric. KD: + serial. S5 = KT45.

Symbols.

Metatheory. Sound and complete with respect to the class of all Kripke frames (Kripke, 1963); the canonical model construction gives completeness directly, and K is trivially canonical since it imposes no frame condition. It is also complete for the far smaller class of finite intransitive trees, which yields the tree model property. Filtration through the subformulas of φ gives the finite model property with a model of size at most 2^|sub(φ)|, hence decidability; Ladner (1977) showed satisfiability to be PSPACE-complete, the same bound as T and S4 and strictly above the NP-completeness of S5. K has Craig interpolation and the Beth definability property. Under the standard translation K is the fragment of first-order logic invariant under bisimulation (van Benthem's characterization theorem, 1976), and it lives inside the two-variable fragment, which explains its decidability. Sahlqvist's theorem applies to every axiom expressible in the Sahlqvist form, so most familiar extensions of K remain canonical and elementary.

Applies to. Modal logic foundation. Provability. Knowledge. Temporal reasoning.

Limitations. K constrains □ only through distribution, so it fixes no reading: □⊥ is satisfiable at dead ends, □A ∧ □¬A is consistent, and □A → ◇A fails. Normality itself is restrictive — closure under necessitation forces knowledge or belief in every validity, the logical omniscience problem, and it makes K unsuitable as it stands for ability, obligation-with-conflicts, or evidence, all of which require neighbourhood or non-normal semantics. Kripke completeness does not extend to normal extensions in general: Thomason (1974) and Fine (1974) exhibited normal modal logics with no class of Kripke frames determining them, and Blok (1978) showed such incompleteness is the typical case among normal extensions. The bisimulation-invariance that makes K decidable also caps its expressive power: it cannot state reachability, cardinality of successors, or the identity of a world, which is why transitive closure, graded and hybrid operators must be added rather than defined.

© 2026 Lingenic LLC