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 FMP. Medvedev logic: no FMP.

Gödel translation: Classical logic embeds via double negation. □A = ¬¬A in modal terms.

Symbols.

Symbol	Unicode	Name	Meaning
IPC	—	Intuitionistic	Bottom
CPC	—	Classical	Top
LC	—	Gödel-Dummett	Linear
KC	—	Jankov	Weak EM

Metatheory. Continuum many intermediate logics. Lattice structure. Kripke completeness varies. Some lack FMP. Decidability varies.

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

Limitations. Too many to catalog. Properties vary wildly. Not all Kripke complete. Classification incomplete.