In mathematical logic, a superintuitionistic logic is a propositional logic extending intuitionistic logic. A logic is a set of propositional formulas with certain closure properties. The logics are partially ordered under containment. A logic is stronger than another iff it contains the other.

Classical logic is the strongest consistent superintuitionistic logic. Thus, the consistent superintuitionistic logics are called intermediate logics, because the logics are intermediate in how many formulas they contain between intuitionistic logic and classical logic.^[1]

Definition

A superintuitionistic logic is a set L of propositional formulas in a countable set of variables p_i 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(p₁, p₂, ..., p_n) is a formula of L, and G₁, G₂, ..., G_n are any formulas, then F(G₁, G₂, ..., G_n) belongs to L (closure under substitution).

Such a logic is intermediate if furthermore

4. L is not the set of all formulas (i.e. the inconsistent logic).

Properties

There exists a continuum of different intermediate logics.

There exists a continuum of different intermediate logics with the disjunction property (DP).

Intermediate logics form a complete lattice, with intuitionistic logic as the bottom and classical logic as the top. It has a unique coatom called SmL. Similarly, superintuitionistic logics form a complete lattice, with intuitionistic logic as the bottom and inconsistent logic as the top. Classical logic is the only coatom.

Syntactics

Many intermediate logics are given by adding one or more axioms to intuitionistic logic (usually denoted as intuitionistic propositional calculus IPC, but also Int, IL or H). Examples include:

• Classical logic (CPC, Cl, CL):

= IPC + ¬¬p → p (Double-negation elimination, DNE)

= IPC + (¬p → p) → p (Consequentia mirabilis)

= IPC + p ∨ ¬p (Principle of excluded middle, PEM)

Immediate generalized variants of the above (but actually equivalent principles over intuitionistic logic) are, respectively,

= IPC + (¬p → ¬q) → (q → p) (inverse contraposition principle)

= IPC + ((p → q) → p) → p (Peirce's principle PP, compare to Consequentia mirabilis)

= IPC + (q → p) → ((¬q → p) → p) (another schema generalizing Consequentia mirabilis)

= IPC + p ∨ (p → q) (following from PEM via principle of explosion)

= IPC + (q → p) → (p ∨ ¬q) (another variant of PEM, see material implication)

• Smetanich's logic (SmL):

= IPC + (¬q → p) → (((p → q) → p) → p) (a conditional PP)

• Gödel-Dummett logic (Dummett 1959) (LC or G, see extensions below):

= IPC + (p → q) ∨ (q → p) (Dirk Gently’s principle, DGP, or linearity)

= IPC + (p → (q ∨ r)) → ((p → q) ∨ (p → r)) (a form of independence of premise IP)

= IPC + ((p ∧ q) → r) → ((p → r) ∨ (q → r)) (Generalized 4th De Morgan's law)

• Bounded depth 2 (BD₂, see generalizations below. Compare with p ∨ (p → q)):

= IPC + p ∨ (p → (q ∨ ¬q))

• Jankov's logic (1968)^[2] or De Morgan logic (KC):

= IPC + ¬¬p ∨ ¬p (weak PEM, a.k.a. WPEM)

= IPC + (p → q) ∨ (¬p → ¬q) (a weak DGP)

= IPC + (p → (q ∨ ¬r)) → ((p → q) ∨ (p → ¬r)) (a variant, with negation, of a form of IP)

= IPC + ¬(p ∧ q) → (¬q ∨ ¬p) (4th De Morgan's law)

= IPC + ¬¬(p ∨ q) → (¬¬p ∨ ¬¬q) (a form of double-negation shift)

• Scott's logic (SL):

= IPC + ((¬¬p → p) → (p ∨ ¬p)) → (¬¬p ∨ ¬p) (a conditional WPEM)

• Kreisel–Putnam logic (KP):

= IPC + (¬p → (q ∨ r)) → ((¬p → q) ∨ (¬p → r)) (the other variant, with negation, of a form of IP)

This list is, for the most part, not any sort of ordering. For example, LC is known not to prove all theorems of SmL, but it does not directly compare in strength to BD₂. Likewise, e.g., KP does not compare to SL. The list of equalities for each logic is by no means exhaustive either. For example, as with WPEM and De Morgan's law, several forms of DGP using conjunction may be expressed.

Even (¬¬p ∨ ¬p) ∨ (¬¬p → p), a further weakening of WPEM, is not a theorem of IPC.

It may also be worth noting that, taking all of intuitionistic logic for granted, the equalities notably rely on explosion. For example, over mere minimal logic, as principle PEM is already equivalent to Consequentia mirabilis, but there does not imply the stronger DNE, nor PP, and is not comparable to DGP.

Going on:

• logics of bounded depth (BD_n):

IPC + p_n ∨ (p_n → (p_n−1 ∨ (p_n−1 → ... → (p₂ ∨ (p₂ → (p₁ ∨ ¬p₁)))...)))

• Gödel n-valued logics (G_n):

LC + BD_n−1

= LC + BC_n−1

• logics of bounded cardinality (BC_n):

${\displaystyle \textstyle \mathbf {IPC} +\bigvee _{i=0}^{n}{\bigl (}\bigwedge _{j<i}p_{j}\to p_{i}{\bigr )}}$

• logics of bounded top width (BTW_n):

${\displaystyle \textstyle \mathbf {IPC} +\bigvee _{i=0}^{n}{\bigl (}\bigwedge _{j<i}p_{j}\to \neg \neg p_{i}{\bigr )}}$

• logics of bounded width, also known as the logic of bounded anti-chains, Ono (1972) (BW_n, BA_n):

${\displaystyle \textstyle \mathbf {IPC} +\bigvee _{i=0}^{n}{\bigl (}\bigwedge _{j\neq i}p_{j}\to p_{i}{\bigr )}}$

• logics of bounded branching (Gabbay & de Jongh, 1974^[3]) (T_n, BB_n):

${\displaystyle \textstyle \mathbf {IPC} +\bigwedge _{i=0}^{n}{\bigl (}{\bigl (}p_{i}\to \bigvee _{j\neq i}p_{j}{\bigr )}\to \bigvee _{j\neq i}p_{j}{\bigr )}\to \bigvee _{i=0}^{n}p_{i}}$

Furthermore:

• Realizability logics
• Medvedev's logic of finite problems (LM, ML):^[4][5][6] defined semantically as the logic of all frames of the form ${\displaystyle \langle {\mathcal {P}}(X)\setminus \{X\},\subseteq \rangle }$ for finite sets X ("Boolean hypercubes without top"), not known to be recursively axiomatizable
• ...

The propositional logics SL and KP do have the disjunction property DP. Kleene realizability logic and the strong Medvedev's logic do have it as well. There is no unique maximal logic with DP on the lattice. Note that if a consistent theory validates WPEM but still has independent statements when assuming PEM, then it cannot have DP.

Semantics

Kripke semantics is used to semantically study intuitionistic logic. Similarly, other intermediate logics can be studied by semantic models. For example, Gödel–Dummett logic has a simple semantic characterization in terms of total orders.

Given a Heyting algebra H, the set of propositional formulas that are valid in H is an intermediate logic. Conversely, given an intermediate logic it is possible to construct its Lindenbaum–Tarski algebra, which is then a Heyting algebra.

An intuitionistic Kripke frame F is a partially ordered set, and a Kripke model M is a Kripke frame with valuation such that ${\displaystyle \{x\mid M,x\Vdash p\}}$ is an upper subset of F. The set of propositional formulas that are valid in F is an intermediate logic. Given an intermediate logic L it is possible to construct a Kripke model M such that the logic of M is L (this construction is called the canonical model). A Kripke frame with this property may not exist, but a general frame always does.

Relation to modal logics

Let A be a propositional formula. The Gödel–Tarski translation of A is defined recursively as follows:

• ${\displaystyle T(p_{n})=\Box p_{n}}$
• ${\displaystyle T(\neg A)=\Box \neg T(A)}$
• ${\displaystyle T(A\land B)=T(A)\land T(B)}$
• ${\displaystyle T(A\vee B)=T(A)\vee T(B)}$
• ${\displaystyle T(A\to B)=\Box (T(A)\to T(B))}$

If M is a modal logic extending S4 then ρM = {A | T(A) ∈ M} is a superintuitionistic logic, and M is called a modal companion of ρM. In particular:

• IPC = ρS4
• KC = ρS4.2
• LC = ρS4.3
• CPC = ρS5

For every intermediate logic L there are many modal logics M such that L = ρM.

See also

• List of logic systems

Notes

References

• Chagrov, Alexander; Zakharyaschev, Michael (1997). Modal Logic. Oxford: Clarendon Press. p. 605. ISBN 9780198537793.
• Dragalin, Albert (1988). Mathematical Intuitionism: Introduction to Proof Theory. Providence, R.I.: American Mathematical Society. p. 228. ISBN 0-8218-4520-9.

• Medvedev, Yu T. (1962). "[Finite Problems]" (PDF). Soviet Mathematics (in Russian). 3 (1): 227–230. doi:10.2307/2272084. JSTOR 2272084. English translation of XXXVIII 356(20) by Elliott Mendelson.
• Medvedev, Yu T. (1963). "[Interpretation of logical formulas by means of finite problems and its relation to the readability theory]" (PDF). Soviet Mathematics (in Russian). 4 (1): 180–183. doi:10.2307/2272084. JSTOR 2272084. English translation of XXXVIII 356(21) by Sue Ann Walker.
• Medvedev, Yu T. (1966). "[Interpretation of logical formulas by means of finite problems]" (PDF). Soviet Mathematics (in Russian). 7 (4): 857–860. doi:10.2307/2272084. JSTOR 2272084. English translation of XXXVIII 356(22) by Sue Ann Walker
• Terwijn, Sebastiaan A. (2006). "Constructive Logic and the Medvedev Lattice". Notre Dame Journal of Formal Logic. 47 (1): 73–82. doi:10.1305/ndjfl/1143468312.
• Umezawa, Toshio (June 1959). "On logics intermediate between intuitionistic and classical predicate logic". Journal of Symbolic Logic. 24 (2): 141–153. doi:10.2307/2964756. JSTOR 2964756. S2CID 13357205.
• Gabbay, D. M.; De Jongh, D. H. J. (1974). "A sequence of decidable finitely axiomatizable intermediate logics with the disjunction property". Journal of Symbolic Logic. 39 (1): 67‒78. doi:10.2307/2272344. JSTOR 2272344.

External links

• "Intermediate logic", Encyclopedia of Mathematics, EMS Press, 2001 [1994]