nLab intuitionistic logic

Contents

Context

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axiom

Removing axioms

Contents

Idea

Intuitionistic logic was introduced by Arend Heyting as a logic for Brouwer's intuitionistic mathematics. It applies more generally to constructive mathematics and so may also be called constructive logic.

Beware the terminological ambiguity: Some people insist that “intuitionistic logic” refers to Brouwerian intuitionism, which includes axioms that contradict classical logic; but other people use “intuitionistic” to mean the same as what in other contexts is called “constructive”, i.e. mathematics without the principle of excluded middle or the axiom of choice but nothing added that contradicts them. Some people (particularly material set theorists) use “constructive” to mean predicative constructive and “intuitionistic” to mean impredicative constructive.

Definition

Intuitionistic logic is most easily described as classical logic without the principle of excluded middle (A¬A\vdash A \vee \neg{A}) or the double-negation rule (¬¬AA\neg\neg{A} \vdash A). It may also be defined by starting with Gentzen's sequent calculus for classical logic (with ¬\neg but not \bot) and restricting to sequents ΓΔ\Gamma \vdash \Delta where Δ\Delta may contain at most one formula, or by starting with sequent calculus with \bot and restricting to such sequents where Δ\Delta must contain exactly one formula.

Properties

Double negation

The double negation translation says that a proposition PP is provable in classical logic precisely if its double negation ¬¬P\not \not P is provable in constructive logic

Disjunction property

Unlike classical logic, intuitionistic logic has the disjunction? and existence? properties: any proof of AB\vdash A \vee B must contain a proof of either A\vdash A or B\vdash B, and similarly any proof of x.F(x)\vdash \exists x.\,F(x) must construct a term tt and a proof of F(t)\vdash F(t). These properties are what justify our calling intuitionistic logic ‘constructive’.

On the other hand, (classical) Peano arithmetic is conservative over (intuitionistic) Heyting arithmetic when restricted to Π 1 0\Pi^0_1 formulas; that is, formulas of the form x:N.y:N.F(x,y)\forall x\colon N.\, \exists y\colon N.\, F(x,y). Roughly speaking, classical logic can be just as ‘constructive’ as intuitionistic logic as far as proving the totality of functions \mathbb{N} \to \mathbb{N} is concerned.

Classicality principles

The principle of excluded middle is not provable in intuitionistic logic, and if we assume it then the logic becomes classical logic. But there are other principles that are provable classically but not intuitionistically, but which are weaker than full PEM, such as

categoryfunctorinternal logictheoryhyperdoctrinesubobject posetcoverageclassifying topos
finitely complete categorycartesian functorcartesian logicessentially algebraic theory
lextensive categorydisjunctive logic
regular categoryregular functorregular logicregular theoryregular hyperdoctrineinfimum-semilatticeregular coverageregular topos
coherent categorycoherent functorcoherent logiccoherent theorycoherent hyperdoctrinedistributive latticecoherent coveragecoherent topos
geometric categorygeometric functorgeometric logicgeometric theorygeometric hyperdoctrineframegeometric coverageGrothendieck topos
Heyting categoryHeyting functorintuitionistic first-order logicintuitionistic first-order theoryfirst-order hyperdoctrineHeyting algebra
De Morgan Heyting categoryintuitionistic first-order logic with weak excluded middleDe Morgan Heyting algebra
Boolean categoryclassical first-order logicclassical first-order theoryBoolean hyperdoctrineBoolean algebra
star-autonomous categorymultiplicative classical linear logic
symmetric monoidal closed categorymultiplicative intuitionistic linear logic
cartesian monoidal categoryfragment {&,}\{\&, \top\} of linear logic
cocartesian monoidal categoryfragment {,0}\{\oplus, 0\} of linear logic
cartesian closed categorysimply typed lambda calculus

References

The observation that the poset of open subsets of a topological space (the internal logic of the sheaf topos) serves as a model for intuitionistic logic is apparently originally due to

  • Alfred Tarski, Der Aussagenkalkül und die Topologie, Fundamenta Mathematicae 31 (1938), pp. 103-134.

A textbook account in the context of programming languages is in section 30 of

Last revised on November 16, 2022 at 06:10:17. See the history of this page for a list of all contributions to it.