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).
Definition.
A superintuitionistic logic is a set "L" of propositional formulas in a countable set of
variables "p""i" satisfying the following properties:
Such a logic is intermediate if furthermore
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:
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–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 formula_4 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:
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:
For every intermediate logic "L" there are many modal logics "M" such that "L" = ρ"M".