# nLab intuitionistic logic

foundations

## Foundational axioms

foundational axiom

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

## Definition

Intuitionistic logic is most easily described as classical logic without the principle of the excluded middle ($\vdash A \vee \neg{A}$) or the double-negation rule ($\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

Unlike classical logic, intuitionistic logic has the disjunction? and existence? properties: any proof of $\vdash A \vee B$ must contain a proof of either $\vdash A$ or $\vdash B$, and similarly any proof of $\vdash \exists x.\,F(x)$ must construct a term $t$ and a proof of $\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 $\Pi^0_1$ formulas; that is, formulas of the form $\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.

## 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, FundamentaMathemeticae 31 (1938), pp. 103–134.

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

Revised on December 4, 2012 21:57:02 by Urs Schreiber (131.174.40.191)