Intermediate Logics

Origin. Gödel (1932) showed IPC has no finite characteristic matrix and exhibited the first infinite chain; Jaśkowski (1936) gave a characteristic matrix sequence. Dummett (1959) axiomatized LC; Umezawa (1959) and Hosoi (1967) began the systematic study; Jankov (1968) proved the lattice has the cardinality of the continuum. Kuznetsov and Maksimova developed the theory from the 1970s. Logics between intuitionistic and classical. Superintuitionistic logics. Uncountably many exist. Lattice structure under extension.

Models. Extend intuitionistic logic (IPC). Contained in classical logic (CPC). IPC ⊂ L ⊂ CPC. Characterized by Kripke frames with properties.

Formalism.

Definition: L intermediate iff IPC ⊆ L ⊆ CPC Closed under modus ponens and substitution.

Notable intermediate logics:

Gödel-Dummett (LC): IPC + (φ → ψ) ∨ (ψ → φ) Linear Kripke frames.

Kreisel-Putnam (KP): IPC + (¬φ → ψ ∨ χ) → (¬φ → ψ) ∨ (¬φ → χ)

Jankov (KC): IPC + ¬φ ∨ ¬¬φ Weak excluded middle.

Scott (SL): IPC + ((¬¬φ → φ) → φ ∨ ¬φ) → ¬φ ∨ ¬¬φ

Lattice structure: Intermediate logics form a lattice. IPC is bottom, CPC is top. Uncountably many logics.

Finite model property: Not all have it. There are continuum many intermediate logics without the FMP, and Shehtman (1977) exhibited one that is not Kripke complete at all. Medvedev logic does have the FMP — it is defined by a class of finite frames. What is open for Medvedev logic is recursive axiomatizability, and with it decidability.

Two distinct translations, often conflated: Gödel–Gentzen (1933), CPC into IPC: prefix ¬¬ and rewrite ∨ and ∃ away. A is classically provable iff its negative translation is intuitionistically provable. Gödel (1933), IPC into S4: prefix □ to every subformula. A is intuitionistically provable iff its □-translation is provable in S4. The first goes down, the second goes sideways; □A is not ¬¬A.

Modal companions: The Blok–Esakia theorem: the lattice of intermediate logics is isomorphic to the lattice of normal extensions of Grzegorczyk's logic Grz. Every intermediate logic has a least and a greatest modal companion.

Symbols.

Symbol	Unicode	Name	Meaning
IPC	—	Intuitionistic propositional calculus	The bottom of the lattice
CPC	—	Classical propositional calculus	The top of the lattice
LC	—	Gödel–Dummett logic	IPC + linearity; complete for linear frames
KC	—	Jankov's logic	IPC + weak excluded middle; complete for directed frames
KP	—	Kreisel–Putnam logic	IPC + the KP axiom; has the disjunction property
SL	—	Scott's logic	IPC + Scott's axiom
ML	—	Medvedev logic	The logic of finite problems
Grz	—	Grzegorczyk's logic	The modal logic whose extensions match the intermediate logics
S4	—	Modal logic S4	Target of the Gödel □-translation
⊆	U+2286	Subset of or equal to	Inclusion of logics
⊂	U+2282	Proper subset of	Strict inclusion, as in IPC ⊂ L ⊂ CPC
L	—	An intermediate logic	The variable ranging over the lattice
φ, ψ, χ	—	Formula metavariables	Schematic letters in the axioms
¬	U+00AC	Not sign / Negation	Occurs in KC, KP and Scott's axiom
∨	U+2228	Logical or / Disjunction	Occurs in every axiom listed
→	U+2192	Rightwards arrow / Implication	Occurs in every axiom listed
□	U+25A1	White square / Necessity	The modal operator of the Gödel translation

Metatheory. The intermediate logics form a complete lattice with IPC at the bottom and CPC at the top, and Jankov (1968) showed it has the cardinality of the continuum, so all but countably many are not recursively axiomatizable at all. Jankov's characteristic formulas are the tool: each finite subdirectly irreducible Heyting algebra yields a formula refuted exactly in the varieties containing it, which is how the continuum is produced and how splittings of the lattice are computed. CPC is the unique maximal consistent intermediate logic, so the lattice has a single co-atom at the top and continuum-many branching below it. The Blok–Esakia theorem makes the lattice isomorphic to the lattice of normal extensions of Grz, transferring modal results wholesale. Maksimova (1977) showed only finitely many intermediate logics have Craig interpolation, so the property is exceptional rather than typical. Kripke completeness, the finite model property, decidability and the disjunction property are all independent of one another and none is inherited by extensions.

Applies to. Foundations of constructivism. Proof theory. Semantics of programming. Intermediate strength reasoning.

Limitations. Because the lattice has the cardinality of the continuum and there are only countably many recursive axiom sets, almost every intermediate logic is not recursively axiomatizable, hence not presentable at all — the family is a mathematical object rather than a catalogue of usable systems. Kripke semantics is not adequate for it: Shehtman (1977) exhibited a Kripke-incomplete intermediate logic, so completeness must be proved logic by logic, with Heyting algebras or general frames as the fallback. Good behaviour is the exception rather than the rule: only finitely many have Craig interpolation, continuum many lack the finite model property, and none of completeness, the finite model property, decidability or the disjunction property can be read off an axiomatization. Even a well-studied member resists — whether Medvedev logic is recursively axiomatizable, and hence whether it is decidable, has been open since Medvedev posed it in 1962.