foundations of mathematics Intuitionistic logic

The Dutch mathematician L.E.J. Brouwer (1881–1966) in the early 20th century had the fundamental insight that such nonconstructive arguments will be avoided if one abandons a principle of classical logic which lies behind De Morgan’s laws. This is the principle of the excluded third (or excluded middle), which asserts that, for every proposition p, either p or not p; and equivalently that, for every p, not not p implies p. This principle is basic to classical logic and had already been enunciated by Aristotle, though with some reservations, as he pointed out that the statement “there will be a sea battle tomorrow” is neither true nor false.

Brouwer did not claim that the principle of the excluded third always fails, only that it may fail in the presence of infinite sets. Of two natural numbers x and y one can always decide whether x = y or x ≠ y, but of two real numbers this may not be possible, as one might have to know an infinite number of digits of their decimal expansions. Similar objections apply to De Morgan’s laws, a consequence of the principle of the excluded third. For a finite set A, if it has been shown that the assertion ∀_{x ∊ A}¬ϕ(x) leads to a contradiction, ∃_{x ∊ A}ϕ(x) can be verified by looking at each element of A in turn; i.e., the statement that no members of a given set have a certain property can be disproved by examining in turn each element of the set. For an infinite set A, there is no way in which such an inspection can be carried out.

Brouwer’s philosophy of mathematics is called intuitionism. Although Brouwer himself felt that mathematics was language-independent, his disciple Arend Heyting (1898–1980) set up a formal language for first-order intuitionistic arithmetic. Some of Brouwer’s later followers even studied intuitionistic type theory (see below Intuitionistic type theories), which differs from classical type theory only by the absence of a single axiom (double negation):∀_{x ∊ Ω}(¬¬x ⊃ x), where Ω is the type of truth-values.

While it cannot be said that many practicing mathematicians have followed Brouwer in rejecting this principle on philosophical grounds, it came as a great surprise to people working in category theory that certain important categories called topoi (singular: topos; see below Topos theory) have associated with them a language that is intuitionistic in general. In consequence of this fact, a theorem about sets proved constructively was immediately seen to be valid not only for sets but also for sheaves, which, however, lie beyond the scope of this article.

The moderate form of intuitionism considered here embraces Kronecker’s constructivism but not the more extreme position of finitism. According to this view, which goes back to Aristotle, infinite sets do not exist, except potentially. In fact, it is precisely in the presence of infinite sets that intuitionists drop the classical principle of the excluded third.

An even more extreme position, called ultrafinitism, maintains that even very large numbers do not exist, say numbers greater than 10⁽¹⁰¹⁰⁾. Of course, the vast majority of mathematicians reject this view by referring to 10⁽¹⁰¹⁰⁾ + 1, but the true believers have subtle ways of getting around this objection, which, however, lie beyond the scope of this discussion.