Jankov Logic (KC, Weak Excluded Middle)

Origin. V. A. Jankov, "The calculus of the weak law of excluded middle" (Izvestiya, 1968), which named and studied it; the axiom appears earlier in Gödel and in Kolmogorov's circle. Jankov's characteristic formulas (1963, 1969) — the tool that made the lattice of intermediate logics tractable — came out of the same work.

Models. Intuitionistic logic plus the weak law of excluded middle: not "p or not p", but "not p or not not p". The addition is small and its consequences are not: KC is exactly the logic of directed frames, it is intermediate, and it loses the disjunction property while gaining nothing constructively — which makes it the standard example that a natural-looking axiom can break the property intuitionism cared about most.

Formalism.

The axiom: KC = IPC + (¬p ∨ ¬¬p) Equivalently: IPC + De Morgan's law ¬(p ∧ q) → (¬p ∨ ¬q). Hence the other name: De Morgan logic.

Semantics: Complete for directed (confluent) Kripke frames: for all w, u, v with wRu and wRv, there is z with uRz and vRz. Directedness is a first-order frame condition, and the axiom is Sahlqvist — so KC is canonical and has the finite model property.

The disjunction property fails: ⊢_KC ¬p ∨ ¬¬p ⊬_KC ¬p and ⊬_KC ¬¬p A theorem whose disjuncts are both underivable. IPC has no such theorem; KC does.

Position: IPC ⊊ KC ⊊ CL KC ⊆ ML: Medvedev's logic validates weak excluded middle. KC and KP are incomparable: KP ⊬ ¬p ∨ ¬¬p, KC ⊬ the KP axiom.

The negative fragment: KC and IPC have the same negative fragment — the same theorems built from ¬, ∧, →. So the weak law adds nothing about negation as such, only about its distribution over disjunction.

Jankov's characteristic formulas: For each finite subdirectly irreducible Heyting algebra A, a formula χ(A) such that a logic L refutes χ(A) iff A is not a model of L. This is what let Jankov prove the lattice of intermediate logics has continuum many members (1968) — the technique matters more than the logic.

Symbols.

Metatheory. KC is the cleanest demonstration that the disjunction property is fragile: one Sahlqvist axiom with a first-order frame condition destroys it, and the logic that results is still intermediate and still constructive in every other respect. The characteristic-formula technique from the same papers is the more consequential contribution — it converts questions about the lattice of intermediate logics into questions about finite Heyting algebras, and it is how the continuum-many result and most subsequent lattice theory were proved. Under Esakia duality, KC's directed frames are Esakia spaces with a least element in every closed upset.

Applies to. The lattice of intermediate logics. Weak counterexamples and the analysis of negation in constructive settings. Jankov formulas, which are the standard tool for splitting the lattice. Medvedev's logic, which validates KC and is where the axiom becomes forced rather than added.

Limitations. The axiom is not constructively acceptable — Brouwer would reject ¬p ∨ ¬¬p as readily as p ∨ ¬p, since neither disjunct is decided — so KC is a formal object rather than a position anyone holds. Its interest is comparative: it exists to mark a point in the lattice and to show what the disjunction property costs.

© 2026 Lingenic LLC