Intermediate logic
Encyclopedia
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).
variables pi satisfying the following properties:
Such a logic is intermediate if furthermore
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 order
s.
H, the set of propositional formula
s 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 (this construction is called canonical model). A Kripke frame with this property may not exist, but a general frame
always does.
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.
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, a superintuitionistic logic is a propositional logic extending intuitionistic logic
Intuitionistic logic
Intuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...
. Classical logic
Classical logic
Classical logic identifies a class of formal logics that have been most intensively studied and most widely used. The class is sometimes called standard logic as well...
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 ofvariables pi 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 ponensModus ponensIn classical logic, modus ponendo ponens or implication elimination is a valid, simple argument form. It is related to another valid form of argument, modus tollens. Both Modus Ponens and Modus Tollens can be mistakenly used when proving arguments...
); - if F(p1, p2, ..., pn) is a formula of L, and G1, G2, ..., Gn are any formulas, then F(G1, G2, ..., Gn) 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 continuumCardinality of the continuum
In set theory, the cardinality of the continuum is the cardinality or “size” of the set of real numbers \mathbb R, sometimes called the continuum. It is an infinite cardinal number and is denoted by |\mathbb R| or \mathfrak c ....
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): = =
- the logic of the weak excluded middle (KC, Jankov's logic, De Morgan logic):
- GödelKurt GödelKurt Friedrich Gödel was an Austrian logician, mathematician and philosopher. Later in his life he emigrated to the United States to escape the effects of World War II. One of the most significant logicians of all time, Gödel made an immense impact upon scientific and philosophical thinking in the...
–DummettMichael DummettSir Michael Anthony Eardley Dummett FBA D.Litt is a British philosopher. He was, until 1992, Wykeham Professor of Logic at the University of Oxford...
logic (LC, G): - KreiselGeorg KreiselGeorg Kreisel FRS is an Austrian-born mathematical logician who has studied and worked in Great Britain and America. Kreisel came from a Jewish background; his family sent him to England before the Anschluss, where he studied mathematics at Trinity College, Cambridge and then, during World War...
–PutnamHilary PutnamHilary Whitehall Putnam is an American philosopher, mathematician and computer scientist, who has been a central figure in analytic philosophy since the 1960s, especially in philosophy of mind, philosophy of language, philosophy of mathematics, and philosophy of science...
logic (KP): - Medvedev's logic of finite problems (LM, ML): defined semantically as the logic of all framesKripke semanticsKripke semantics is a formal semantics for non-classical logic systems created in the late 1950s and early 1960s by Saul Kripke. It was first made for modal logics, and later adapted to intuitionistic logic and other non-classical systems...
of the form
for finite sets X ("Boolean hypercubes without top"), not known to be recursively axiomatizable - realizabilityRealizabilityRealizability is a part of proof theory which can be used to handle information about formulas instead of about the proofs of formulas. A natural number n is said to realize a statement in the language of arithmetic of natural numbers...
logics - ScottDana ScottDana Stewart Scott is the emeritus Hillman University Professor of Computer Science, Philosophy, and Mathematical Logic at Carnegie Mellon University; he is now retired and lives in Berkeley, California...
's logic (SL): - Smetanich's logic (SmL):
- logics of bounded cardinality (BCn):
- logics of bounded width, also known as the logic of bounded anti-chains (BWn, BAn):
- logics of bounded depth (BDn):
- logics of bounded top width (BTWn):
- logics of bounded branching (Tn, BBn):
- Gödel n-valued logics (Gn): LC + BCn−1 = LC + BDn−1
Superintuitionistic or intermediate logics form a complete lattice
Complete lattice
In mathematics, a complete lattice is a partially ordered set in which all subsets have both a supremum and an infimum . Complete lattices appear in many applications in mathematics and computer science...
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
Kripke semantics
Kripke semantics is a formal semantics for non-classical logic systems created in the late 1950s and early 1960s by Saul Kripke. It was first made for modal logics, and later adapted to intuitionistic logic and other non-classical systems...
. For example, Gödel–Dummett logic has a simple semantic characterization in terms of total order
Total order
In set theory, a total order, linear order, simple order, or ordering is a binary relation on some set X. The relation is transitive, antisymmetric, and total...
s.
Semantics
Given a Heyting algebraHeyting algebra
In mathematics, a Heyting algebra, named after Arend Heyting, is a bounded lattice equipped with a binary operation a→b of implication such that ∧a ≤ b, and moreover a→b is the greatest such in the sense that if c∧a ≤ b then c ≤ a→b...
H, the set of propositional formula
Propositional formula
In propositional logic, a propositional formula is a type of syntactic formula which is well formed and has a truth value. If the values of all variables in a propositional formula are given, it determines a unique truth value...
s 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
Partially ordered set
In mathematics, especially order theory, a partially ordered set formalizes and generalizes the intuitive concept of an ordering, sequencing, or arrangement of the elements of a set. A poset consists of a set together with a binary relation that indicates that, for certain pairs of elements in the...
, and a Kripke model M is a Kripke frame with valuation such that
is an upper subsetUpper set
In mathematics, an upper set of a partially ordered set is a subset U with the property that x is in U and x≤y imply y is in U....
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
General frame
In logic, general frames are Kripke frames with an additional structure, which are used to model modal and intermediate logics...
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
Modal logic
Modal logic is a type of formal logic that extends classical propositional and predicate logic to include operators expressing modality. Modals — words that express modalities — qualify a statement. For example, the statement "John is happy" might be qualified by saying that John is...
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.