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 has the disjunction property, so weak excluded middle is not among its theorems. 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.

Symbol	Unicode	Name	Meaning
KC	—	Jankov's logic	IPC + weak excluded middle
¬p ∨ ¬¬p	—	Weak excluded middle	The axiom, in full
χ	U+03C7	Small letter chi	χ(A) is the Jankov formula of the algebra A
¬	U+00AC	Not sign / Negation	The only connective the axiom really concerns
∨	U+2228	Logical or / Disjunction	The connective across which negation distributes
∧	U+2227	Logical and / Conjunction	Occurs in the De Morgan formulation
→	U+2192	Rightwards arrow / Implication	Occurs in the De Morgan formulation
R	—	Accessibility relation	Directed in KC's frames
w, u, v, z	—	Worlds	Points of a Kripke frame, in the directedness condition
A	—	Heyting algebra	Finite and subdirectly irreducible, in Jankov's construction
⊢	U+22A2	Right tack / Turnstile	Derivability, subscripted by the logic
⊬	U+22AC	Does not prove	Underivability of each disjunct
⊊	U+228A	Subset of with not equal to	Proper inclusion, as in IPC ⊊ KC ⊊ CL
⊄	U+2284	Not a subset of	Non-inclusion, as in KC ⊄ ML
IPC	—	Intuitionistic propositional calculus	The base
CL	—	Classical logic	The top of the interval
KP	—	Kreisel–Putnam logic	Incomparable with KC
ML	—	Medvedev's logic	Does not contain KC

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, from which the disjunction property excludes the axiom.

Limitations. The axiom is not constructively acceptable — neither disjunct of ¬p ∨ ¬¬p is decided, so the BHK reading gives it no proof any more than it gives one to p ∨ ¬p — and with the disjunction property gone KC is not a constructive logic in Kreisel's sense at all, whatever its other properties. It also adds nothing: KC and IPC have the same negative fragment, so the weak law adds no theorem about negation, only about how negation distributes over disjunction, and no new constructive content is reachable. KC is not tabular, being complete for directed frames of unbounded depth, so no finite matrix decides it and the extra axiom brings no computational simplification over IPC. Its position in the lattice is likewise unhelpful for classification, since it is incomparable with Kreisel–Putnam: strengthening IPC in this direction rules out strengthening it in the other.