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).^{[1]}

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*_{1},*p*_{2}, ...,*p*_{n}) is a formula of*L*, and*G*_{1},*G*_{2}, ...,*G*_{n}are any formulas, then*F*(*G*_{1},*G*_{2}, ...,*G*_{n}) 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 and just as many such logics exhibit the disjunction property (DP).
Superintuitionistic or intermediate logics form a complete lattice with intuitionistic logic as the bottom and the inconsistent logic (in the case of superintuitionistic logics) or classical logic (in the case of intermediate logics) as the top. Classical logic is the only coatom in the lattice of superintuitionistic logics; the lattice of intermediate logics also has a unique coatom, namely **SmL**^{[citation needed]}.

The tools for studying intermediate logics are similar to those used for intuitionistic logic, such as Kripke semantics. For example, Gödel–Dummett logic has a simple semantic characterization in terms of total orders. Specific intermediate logics may be given by semantical description.

Others are often 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*→ ¬*q*) → (*q*→*p*) (inverse contraposition principle)- =
**IPC**+ ¬¬*p*→*p*(Double-negation elimination, DNE) - =
**IPC**+ ((*p*→*q*) →*p*) →*p*(Pierce's principle, PP) - =
**IPC**+*p*∨ ¬*p*(Principle of excluded middle, PEM)

- Smetanich's logic (
**SmL**):

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

**IPC**+ (*p*→*q*) ∨ (*q*→*p*) (Dirk Gently’s principle, DGP)- =
**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**_{2}, see generalizations below):

**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)

- Scott's logic (
**SL**):

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

**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**_{2}. 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. It may also be worth noting that, taking all of intuitionistic logic for granted, the equalities notably rely on the principle of explosion. For example, over mere minimal logic PEM does not imply PP, and is not comparable to DGP.

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

Going on:

- logics of bounded depth (
**BD**_{n}):

**IPC**+*p*∨ (_{n}*p*→ (_{n}*p*_{n−1}∨ (*p*_{n−1}→ ... → (*p*_{2}∨ (*p*_{2}→ (*p*_{1}∨ ¬*p*_{1})))...)))

- Gödel
*n*-valued logics (**G**_{n}):

**LC**+**BD**_{n−1}- =
**LC**+**BC**_{n−1}

- logics of bounded cardinality (
**BC**_{n}):

- logics of bounded top width (
**BTW**_{n}):

- logics of bounded width, also known as the logic of bounded anti-chains, Ono (1972) (
**BW**_{n},**BA**_{n}):

- logics of bounded branching, Gabbay & de Jongh (1969, 1974) (
**T**_{n},**BB**_{n}):

Furthermore:

- Realizability logics
- Medvedev's logic of finite problems (
**LM**,**ML**):^{[3]}^{[4]}^{[5]}defined semantically as the logic of all frames of the form for finite sets*X*("Boolean hypercubes without top"), as of 2015^{[update]}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.

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 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.

Main article: Modal companion |

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

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*.