nLab
intuitionistic logic

Intuitionistic logic was introduced by Heyting as a formalism intended to encode Brouwer’s constructivism. It is most easily described as classical logic without the principle of the excluded middle A¬A or the double-negation rule ¬¬AA. It may also be defined by starting with Gentzen's sequent calculus for classical logic (with ¬ but not ) and restricting to sequents ΓΔ where Δ may contain at most one formula, or by starting with sequent calculus with and restricting to such sequents where Δ must contain exactly one formula.

Properties

Unlike classical logic, intuitionistic logic has the disjunction and existence properties: any proof of AB must contain a proof of either A or B, and similarly any proof of x.F(x) must construct a term t and a proof of 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 formulas; that is, formulas of the form x:N.y:N.F(x,y). Roughly speaking, classical logic can be just as ‘constructive’ as intuitionistic logic as far as proving the totality of functions is concerned.