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.

Definition

A superintuitionistic logic is a set L of propositional formulas in a countable set of
variables pi 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 or classical logic 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 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. 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 = 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.