Kreisel-Putnam Logic (KP)

Origin. Georg Kreisel and Hilary Putnam, "Eine Unableitbarkeitsbeweismethode für den intuitionistischen Aussagenkalkül" (Archiv für mathematische Logik, 1957). Constructed to refute a conjecture: Łukasiewicz had proposed that intuitionistic logic is the only intermediate logic with the disjunction property, and KP is the counterexample.

Models. Intuitionistic logic plus one axiom, chosen to be underivable and to preserve the disjunction property. The point is negative and structural: the disjunction property was taken to characterize constructivity, and KP shows it does not — a logic can have it and still prove things Brouwer would not accept.

Formalism.

The axiom: KP = IPC + (¬p → q ∨ r) → ((¬p → q) ∨ (¬p → r))

Disjunction property: ⊢ φ ∨ ψ implies ⊢ φ or ⊢ ψ. KP has it. IPC has it. So the property does not single out IPC. That is the theorem the logic exists for.

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

Semantics: Kripke complete, and the frame condition is not a first-order one — the KP axiom is not Sahlqvist and the frames are characterized by a second-order condition. Finite model property holds.

Extensions with the disjunction property: After KP, the field found continuum-many intermediate logics with the disjunction property (Wroński 1973), so the counterexample was not isolated but typical. Maksimova (1986) classified the intermediate logics with interpolation; KP is not among them.

Symbols.

Metatheory. KP's importance is entirely in what it refutes: Łukasiewicz's conjecture had made the disjunction property a candidate definition of constructivity, and one axiom killed it. Wroński's later result — continuum many intermediate logics with the disjunction property — turned the counterexample into a fact about the lattice, and the search for a syntactic characterization of constructivity moved elsewhere. KP is Kripke complete with the finite model property but fails interpolation, which is the usual pattern: the logics that behave well semantically rarely behave well proof-theoretically.

Applies to. The lattice of intermediate logics. The disjunction property and its relation to constructivity. Counterexample methodology in the study of superintuitionistic logics — Kreisel and Putnam's underivability method is the entry's other contribution.

Limitations. The axiom has no independent motivation: it was reverse-engineered to be underivable while preserving the disjunction property, and nobody has since found a reason to accept it. So KP is a specimen rather than a logic anyone reasons in. The frame condition is second-order, which makes it hard to work with, and interpolation fails.

© 2026 Lingenic LLC