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 or the double-negation rule . 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.
Unlike classical logic, intuitionistic logic has the disjunction and existence properties: any proof of must contain a proof of either or , and similarly any proof of must construct a term and a proof of . 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 formulas; that is, formulas of the form . Roughly speaking, classical logic can be just as ‘constructive’ as intuitionistic logic as far as proving the totality of functions is concerned.