Intuitionistic Logic

Abstract

During the past century, a major debate in the philosophy of mathematics has centered on the question of how to regard noneffective or nonconstructive proofs in mathematics. Is it legitimate to claim to have proven the existence of a number with some property without actually being able, even in principle, to produce one? Is it legitimate to claim to have proven the existence of a function without providing any way to calculate it? L. E. J. Brouwer is perhaps the best known early proponent of an extreme constructivist point of view. He rejected much of early twentieth century mathematics on the grounds that it did not provide acceptable existence proofs. He held that a proof of p ⋁ q must consist of either a proof of p or one of q and that a proof of ∃xP(x) must contain a construction of a witness c and a proof that P(c) is true. At the heart of most nonconstructive proofs lies the law of the excluded middle: For every sentence A, A ⋁ ¬A is true. Based on this law of classical logic one can prove that ∃xP(x) by showing that its negation leads to a contradiction without providing any hint as to how to find an x satisfying P. Similarly, one can prove p ⋁ q by proving ¬ (¬p ∧¬ q) without knowing which of p and q is true.