### Intermediate logics

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

## Definition

A superintuitionistic logic is a set *L* of propositional formulas in a countable set of
variables *p*_{i} satisfying the following properties:

- all axioms of intuitionistic logic belong to
*L*; - 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); - 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

*L*is not the set of all formulas.

## Properties and examples

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^{[1]}):**IPC**+ ¬¬*p*∨ ¬*p* - Gödel–Dummett logic (
**LC**,**G**):**IPC**+ (*p*→*q*) ∨ (*q*→*p*) - 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 $\backslash langle\backslash mathcal\; P(X)\backslash setminus\backslash \{X\backslash \},\backslash subseteq\backslash rangle$ for finite sets*X*("Boolean hypercubes without top"), as of 2010^{[update]}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 (
**BC**_{n}): $\backslash textstyle\backslash mathbf\{IPC\}+\backslash bigvee\_\{i=0\}^n\backslash bigl(\backslash bigwedge\_\{j\}p\_j\backslash to\; p\_i\backslash bigr)\; math>$ - logics of bounded width, also known as the logic of bounded anti-chains (
**BW**_{n},**BA**_{n}): $\backslash textstyle\backslash mathbf\{IPC\}+\backslash bigvee\_\{i=0\}^n\backslash bigl(\backslash bigwedge\_\{j\backslash ne\; i\}p\_j\backslash to\; p\_i\backslash bigr)$ - 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})))...))) - logics of bounded top width (
**BTW**_{n}): $\backslash textstyle\backslash mathbf\{IPC\}+\backslash bigvee\_\{i=0\}^n\backslash bigl(\backslash bigwedge\_\{j\}p\_j\backslash to\backslash neg\backslash neg\; p\_i\backslash bigr)\; math>$ - logics of bounded branching (
**T**_{n},**BB**_{n}): $\backslash textstyle\backslash mathbf\{IPC\}+\backslash bigwedge\_\{i=0\}^n\backslash bigl(\backslash bigl(p\_i\backslash to\backslash bigvee\_\{j\backslash ne\; i\}p\_j\backslash bigr)\backslash to\backslash bigvee\_\{j\backslash ne\; i\}p\_j\backslash bigr)\backslash to\backslash bigvee\_\{i=0\}^np\_i$ - Gödel
*n*-valued logics (**G**_{n}):**LC**+**BC**_{n−1}=**LC**+**BD**_{n−1}

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

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.

## Semantics

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 algebra which is 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 $\backslash \{x\backslash mid\; M,x\backslash Vdash\; p\backslash \}$ 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 *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:

- $T(p\_n)\; =\; \backslash Box\; p\_n$
- $T(\backslash neg\; A)\; =\; \backslash Box\; \backslash neg\; T(A)$
- $T(A\; \backslash and\; B)\; =\; T(A)\; \backslash and\; T(B)$
- $T(A\; \backslash vee\; B)\; =\; T(A)\; \backslash vee\; T(B)$
- $T(A\; \backslash to\; B)\; =\; \backslash Box\; (T(A)\; \backslash 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*.

## References

- Toshio Umezawa. On logics intermediate between intuitionistic and classical predicate logic. Journal of Symbolic Logic, 24(2):141–153, June 1959.
- Alexander Chagrov, Michael Zakharyaschev. Modal Logic. Oxford University Press, 1997.