Intermediate logic

In mathematical logic, a superintuitionistic logic is a propositional logic extending intuitionistic logic. Classical logic is the strongest consistent superintuitionistic logic; thus, consistent superintuitionistic logics are called intermediate logics (the logics are intermediate between intuitionistic logic and classical logic). A superintuitionistic logic is a set L of propositional formulas in a countable set of variables pi satisfying the following properties:

1. all axioms of intuitionistic logic belong to L;
2. if F and G are formulas such that F and F → G both belong to L, then G also belongs to L (closure under modus ponens);
3. if F(p1, p2, ..., pn) is a formula of L, and G1, G2, ..., Gn are any formulas, then F(G1, G2, ..., Gn) belongs to L (closure under substitution). Such a logic is intermediate if furthermore
4. L is not the set of all formulas. There exists a continuum of different intermediate logics. Specific intermediate logics are often constructed by adding one or more axioms to intuitionistic logic, or by a semantical description. Examples of intermediate logics include: intuitionistic logic (IPC, Int, IL, H) classical logic (CPC, Cl, CL): IPC + p ∨ ¬p = IPC + ¬¬p → p = IPC + ((p → q) → p) → p the logic of the weak excluded middle (KC, Jankov's logic, De Morgan logic): IPC + ¬¬p ∨ ¬p Gödel–Dummett logic (LC, G): IPC + (p → q) ∨ (q → p) = IPC + (p → (q ∨ r)) → ((p → q) ∨ (p → r)) Kreisel–Putnam logic (KP): IPC + (¬p → (q ∨ r)) → ((¬p → q) ∨ (¬p → r)) Medvedev's logic of finite problems (LM, ML): defined semantically as the logic of all frames of the form for finite sets X ("Boolean hypercubes without top"), not known to be recursively axiomatizable realizability logics Scott's logic (SL): IPC + ((¬¬p → p) → (p ∨ ¬p)) → (¬¬p ∨ ¬p) Smetanich's logic (SmL): IPC + (¬q → p) → (((p → q) → p) → p) logics of bounded cardinality (BCn): logics of bounded width, also known as the logic of bounded anti-chains (BWn, BAn): logics of bounded depth (BDn): IPC + pn ∨ (pn → (pn−1 ∨ (pn−1 → ... → (p2 ∨ (p2 → (p1 ∨ ¬p1))).