Intuitionism is a philosophy of mathematics that was introduced by theDutch mathematician L.E.J. Brouwer (1881–1966). Intuitionism isbased on the idea that mathematics is a creation of the mind. Thetruth of a mathematical statement can only be conceived via a mentalconstruction that proves it to be true, and the communication betweenmathematicians only serves as a means to create the same mentalprocess in different minds.

This view on mathematics has far reaching implications for the dailypractice of mathematics, one of its consequences being that theprinciple of the excluded middle, \((A \vee \neg A)\), is no longervalid. Indeed, there are propositions, like the Riemann hypothesis,for which there exists currently neither a proof of the statement norof its negation. Since knowing the negation of a statement inintuitionism means that one can prove that the statement is not true,this implies that both \(A\) and \(\neg A\) do not holdintuitionistically, at least not at this moment. The dependence ofintuitionism on time is essential: statements can become provable inthe course of time and therefore might become intuitionistically validwhile not having been so before.

Besides the rejection of the principle of the excluded middle,intuitionism strongly deviates from classical mathematics in theconception of the continuum, which in the former setting has theproperty that all total functions on it are continuous. Thus, unlikeseveral other theories of constructive mathematics, intuitionism isnot a restriction of classical reasoning; it contradicts classicalmathematics in a fundamental way.

Brouwer devoted a large part of his life to the development ofmathematics on this new basis. Although intuitionism has neverreplaced classical mathematics as the standard view on mathematics, ithas always attracted a great deal of attention and is still widelystudied today.

In this entry we concentrate on the aspects of intuitionism that setit apart from other branches of constructive mathematics, and the partthat it shares with other forms of constructivism, such asfoundational theories and models, is discussed only briefly.

• 1. Brouwer
• 2. Intuitionism
  • 2.1 The two acts of intuitionism
  • 2.2 The Creating Subject
• 3. Mathematics
  • 3.1 The BHK-interpretation
  • 3.2 Intuitionistic logic
  • 3.3 The natural numbers
  • 3.4 The continuum
  • 3.5 Continuity axioms
  • 3.6 The bar theorem
  • 3.7 Choice axioms
  • 3.8 Descriptive set theory, topology, and topos theory
• 4. Constructivism
• 5. Meta-mathematics
  • 5.1 Arithmetic
  • 5.2 Analysis
  • 5.3 Lawless sequences
  • 5.4 Formalization of the Creating Subject
  • 5.5 Foundations and models
  • 5.6 Reverse mathematics
• 6. Philosophy
  • 6.1 Phenomenology
  • 6.2 Wittgenstein
  • 6.3 Dummett
  • 6.4 Finitism
• Bibliography
• Academic Tools
• Other Internet Resources
• Related Entries

1. Brouwer

Luitzen Egbertus Jan Brouwer was born in Overschie, the Netherlands.He studied mathematics and physics at the University of Amsterdam,where he obtained his PhD in 1907. In 1909 he became a lecturer at thesame university, where he was appointed full professor in 1912, aposition he held until his retirement in 1951. Brouwer was a brilliantmathematician who did ground-breaking work in topology and becamefamous already at a young age. All his life he was an independent mindwho pursued the things he believed in with ardent vigor, which broughthim in conflict with many a colleague, most notably with DavidHilbert. He had admirers as well, and in his house “thehut” in Blaricum he welcomed many well-known mathematicians ofhis time. To the end of his life he became more isolated, but hisbelief in the truth of his philosophy never wavered. He died in a caraccident at the age of 85 in Blaricum, seven years after the death ofhis wife Lize Brouwer.

At the age of 24 Brouwer wrote the bookLife, Art andMysticism (Brouwer 1905), whose solipsistic content foreshadowshis philosophy of mathematics. In his dissertation the foundations ofintuitionism are formulated for the first time, although not yet underthat name and not in their final form. In the first years after hisdissertation most of Brouwer’s scientific life was devoted totopology, an area in which he is still known for his theory ofdimension and his fixed point theorem. This work is part of classicalmathematics; according to Brouwer’s later view, his fixed pointtheorem does not hold, although an analogue cast in terms ofapproximations can be proved to hold according to his principles.

From 1913 on, Brouwer increasingly dedicated himself to thedevelopment of the ideas formulated in his dissertation into a fullphilosophy of mathematics. He not only refined the philosophy ofintuitionism but also reworked mathematics, especially the theory ofthe continuum and the theory of sets, according to these principles.By then, Brouwer was a famous mathematician who gave influentiallectures on intuitionism at the scientific meccas of that time,Cambridge, Vienna, and Göttingen among them. His philosophy wasconsidered awkward by many, but treated as a serious alternative toclassical reasoning by some of the most famous mathematicians of histime, even when they had a different view on the matter. KurtGödel, who was a Platonist all his life, was one of them. HermannWeyl at one point wrote “So gebe ich also jetzt meinen eigenenVersuch Preis und schließe mich Brouwer an” (Weyl 1921,56). And although he rarely practised intuitionistic mathematics laterin life, Weyl never stopped admiring Brouwer and his intuitionisticphilosophy of mathematics.

The life of Brouwer was laden with conflicts, the most famous onebeing the conflict with David Hilbert, which eventually led toBrouwer’s expulsion from the board of theMathematischeAnnalen. This conflict was part of theGrundlagenstreitthat shook the mathematical society at the beginning of the 20thcentury and that emerged as a result of the appearance of paradoxesand highly nonconstructive proofs in mathematics. Philosophers andmathematicians were forced to acknowledge the lack of anepistemological and ontological basis for mathematics. Brouwer’sintuitionism is a philosophy of mathematics that aims to provide sucha foundation.

2. Intuitionism

2.1 The two acts of intuitionism

According to Brouwer mathematics is a languageless creation of themind. Time is the only a priori notion, in the Kantian sense. Brouwerdistinguishes twoacts of intuitionism:

The first act of intuitionism is:

Completely separating mathematics from mathematical language and hencefrom the phenomena of language described by theoretical logic,recognizing that intuitionistic mathematics is an essentiallylanguageless activity of the mind having its origin in the perceptionof a move of time. This perception of a move of time may be describedas the falling apart of a life moment into two distinct things, one ofwhich gives way to the other, but is retained by memory. If the twoitythus born is divested of all quality, it passes into the empty form ofthe common substratum of all twoities. And it is this commonsubstratum, this empty form, which is the basic intuition ofmathematics. (Brouwer 1981, 4–5)

As will be discussed in the section on mathematics, the first act ofintuitionism gives rise to the natural numbers but implies a severerestriction on the principles of reasoning permitted, most notably therejection of the principle of the excluded middle. Owing to therejection of this principle and the disappearance of the logical basisfor the continuum, one might, in the words of Brouwer, “fearthat intuitionistic mathematics must necessarily be poor and anaemic,and in particular would have no place for analysis” (Brouwer1952, 142). The second act, however, establishes the existence of thecontinuum, a continuum having properties not shared by its classicalcounterpart. The recovery of the continuum rests on the notion ofchoice sequence stipulated in the second act, i.e. on the existence ofinfinite sequences generated by free choice, which therefore are notfixed in advance.

The second act of intuitionism is:

Admitting two ways of creating new mathematical entities: firstly inthe shape of more or less freely proceeding infinite sequences ofmathematical entities previously acquired …; secondly in theshape of mathematical species, i.e. properties supposable formathematical entities previously acquired, satisfying the conditionthat if they hold for a certain mathematical entity, they also holdfor all mathematical entities which have been defined to be“equal” to it …. (Brouwer 1981, 8)

The two acts of intuitionism form the basis of Brouwer’sphilosophy; from these two acts alone Brouwer creates the realm ofintuitionistic mathematics, as will be explained below. Already fromthis basic principles it can be concluded that intuitionism differsfrom Platonism and formalism, because neither does it assume amathematical reality outside of us, nor does it hold that mathematicsis a play with symbols according to certain fixed rules. InBrouwer’s view, language is used to exchange mathematical ideasbut the existence of the latter is independent of the former. Thedistinction between intuitionism and other constructive views onmathematics according to which mathematical objects and argumentsshould be computable, lies in the freedom that the second act allowsin the construction of infinite sequences. Indeed, as will beexplained below, the mathematical implications of the second act ofintuitionism contradict classical mathematics, and therefore do nothold in most constructive theories, since these are in general part ofclassical mathematics.

Thus Brouwer’s intuitionism stands apart from other philosophiesof mathematics; it is based on the awareness of time and theconviction that mathematics is a creation of the free mind, and ittherefore is neither Platonism nor formalism. It is a form ofconstructivism, but only so in the wider sense, since manyconstructivists do not accept all the principles that Brouwer believedto be true.

2.2 The Creating Subject

The two acts of intuitionism do not in themselves exclude apsychological interpretation of mathematics. Although Brouwer onlyoccasionally addressed this point, it is clear from his writings thathe did consider intuitionism to be independent of psychology.Brouwer’s introduction of theCreating Subject (Brouwer1948) as an idealized mind in which mathematics takes place alreadyabstracts away from inessential aspects of human reasoning such aslimitations of space and time and the possibility of faulty arguments.Thus the intersubjectivity problem, which asks for an explanation ofthe fact that human beings are able to communicate, ceases to exist,as there exists only one Creating Subject. In the literature, also thenameCreative Subject is used for Creating Subject, but hereBrouwer’s terminology is used. In (Niekus 2010), it is arguedthat Brouwer’s Creating Subject does not involve an idealizedmathematician. For a phenomenological analysis of the Creating Subjectas a transcendental subject in the sense of Husserl see (van Atten2007).

Brouwer used arguments that involve the Creating Subject to constructcounterexamples to certain intuitionistically unacceptable statements.Where the weak counterexamples, to be discussed below, only show thatcertain statements cannot, at present, be accepted intuitionistically,the notion of the idealized mind proves certain classical principlesto be false. An example is given in Section 5.4 on the formalizationof the notion of the Creating Subject. There it is also explained thatthe following principle, known asKripke’s Schema, canbe argued for in terms of the Creating Subject:

InKS, \(A\) ranges over formulas and \( \alpha\) ranges overchoice sequences, which are sequences of natural numbers produced bythe Creating Subject, who chooses their elements one-by-one. Choicesequences and Kripke’s Schema are discussed further in Section3.4.

In most philosophies of mathematics, for example in Platonism,mathematical statements are tenseless. In intuitionism truth andfalsity have a temporal aspect; an established fact will remain so,but a statement that becomes proven at a certain point in time lacks atruth-value before that point. In said formalization of the notion ofCreating Subject, which was not formulated by Brouwer but only laterby others, the temporal aspect of intuitionism is conspicuouslypresent.

Important as the arguments using the notion of Creating Subject mightbe for the further understanding of intuitionism as a philosophy ofmathematics, its role in the development of the field has been lessinfluential than that of the two acts of intuitionism, which directlylead to the mathematical truths Brouwer and those coming after himwere willing to accept.

3. Mathematics

Although Brouwer’s development of intuitionism played animportant role in the foundational debate among mathematicians at thebeginning of the 20th century, the far reaching implications of hisphilosophy for mathematics became only apparent after many years ofresearch. The two most characteristic properties of intuitionism arethe logical principles of reasoning that it allows in proofs and thefull conception of the intuitionistic continuum. Only as far as thelatter is concerned, intuitionism becomes incomparable with classicalmathematics. In this entry the focus is on those principles ofintuitionism that set it apart from other mathematical disciplines,and therefore its other constructive aspects will be treated in lessdetail.

3.1 The BHK-interpretation

In intuitionism, knowing that a statementA is true meanshaving a proof of it. In 1934 Arend Heyting, who had been a student ofBrouwer, introduced a form of what became later known as theBrouwer-Heyting-Kolmogorov-interpretation, which captures themeaning of the logical symbols in intuitionism, and in constructivismin general as well. It defines in an informal way what anintuitionistic proof should consist of by indicating how theconnectives and quantifiers should be interpreted.

• \(\bot\) is not provable.
• A proof of \(A\wedge B\) consists of a proof of \(A\) and a proofof \(B\).
• A proof of \(A \vee B\) consists of a proof of \(A\) or a proof of\(B\).
• A proof of \(A \rightarrow B\) is a construction which transformsany proof of \(A\) into a proof of \(B\).
• A proof of \(\exists x A(x)\) is given by presenting an element\(d\) of the domain and a proof of \(A(d)\).
• A proof of \(\forall x A(x)\) is a construction which transformsevery proof that \(d\) belongs to the domain into a proof of\(A(d)\).

The negation \(\neg A\) of a formula \(A\) is proven once it has beenshown that there cannot exist a proof of \(A\), which means providinga construction that derives falsum from any possible proof of \(A\).Thus \(\neg A\) is equivalent to \(A \rightarrow \bot\). TheBHK-interpretation is not a formal definition because the notion ofconstruction is not defined and therefore open to differentinterpretations. Nevertheless, already on this informal level one isforced to reject one of the logical principles ever-present inclassical logic: the principle of the excluded middle \((A\vee \negA)\). According to the BHK-interpretation this statement holdsintuitionistically if the Creating Subject knows a proof of \(A\) or aproof that \(A\) cannot be proved. In the case that neither for \(A\)nor for its negation a proof is known, the statement \((A \vee \negA)\) does not hold. The existence of open problems, such as theGoldbach conjecture or the Riemann hypothesis, illustrates this fact.But once a proof of \(A\) or a proof of its negation is found, thesituation changes, and for this particular \(A\) the principle \((A\vee \neg A)\) is true from that moment on.

3.2 Intuitionistic logic

Brouwer rejected the principle of the excluded middle on the basis ofhis philosophy, but Arend Heyting was the first to formulate acomprehensive logic of principles acceptable from an intuitionisticpoint of view. Intuitionistic logic, which is the logic of most otherforms of constructivism as well, is often referred to as“classical logic without the principle of the excludedmiddle”. It is denoted by IQC, which stands for IntuitionisticQuantifier Logic, but other names occur in the literature as well. Apossible axiomatization in Hilbert style consists of theprinciples

with the usual side conditions for the last two axioms, and the ruleModus Ponens,

as the only rule of inference. Intuitionistic logic has been an objectof investigation ever since Heyting formulated it. Already at thepropositional level it has many properties that sets it apart fromclassical logic, such as the Disjunction Property:

This principle is clearly violated in classical logic, becauseclassical logic proves \((A \vee \neg A)\) also for formulas that areindependent of the logic, i.e. for which both \(A\) and \(\neg A\) arenot a tautology. The inclusion of the principle Ex Falso SequiturQuodlibet, \((\bot \rightarrow A)\), in intuitionistic logic is apoint of discussion for those studying Brouwer’s remarks on thesubject; in van Atten 2008, it is argued that the principle is notvalid in Intuitionism and that the logical principles valid accordingto Brouwer’s views are those of relevance logic. See van Dalen2004 for more on Brouwer and Ex Falso Sequitur Quodlibet.

Although till today all the logic used in intuitionistic reasoning iscontained inIQC, it is in principle conceivable that at somepoint there will be found a principle acceptable from theintuitionistic point of view that is not covered by this logic. Formost forms of constructivism the widely accepted view is that thiswill not ever be the case, and thusIQC is considered to bethe logic of constructivism. For intuitionism the situationis less clear because it cannot be excluded that at some point ourintuitionistic understanding might lead us to new logical principlesthat we did not grasp before.

One of the reasons for the widespread use of intuitionistic logic isthat it is well-behaved both from the proof-theoretic as themodel-theoretic point of view. There exist a great many proof systemsfor it, such as Gentzen calculi and natural deduction systems, as wellas various forms of semantics, such as Kripke models, Beth models,Heyting algebras, topological semantics and categorical models.Several of these semantics are, however, only classical means to studyintuitionistic logic, for it can be shown that an intuitionisticcompleteness proof with respect to them cannot exist (Kreisel 1962).It has, however, been shown that there are alternative but a littleless natural models with respect to which completeness does holdconstructively (Veldman 1976). The constructive character ofintuitionistic logic becomes particularly clear in the Curry-Howardisomorphism that establishes a correspondence between derivations inthe logic and terms in simply typed \(\lambda\)-calculus, that is,between proofs and computations. The correspondence preservesstructure in that reduction of terms correspond to normalization ofproofs.

3.3 The natural numbers

The existence of the natural numbers is given by the first act ofintuitionism, that is by the perception of the movement of time andthe falling apart of a life moment into two distinct things: what was,1, and what is together with what was, 2, and from there to 3, 4, …In contrast to classical mathematics, in intuitionism all infinity isconsidered to be potential infinity. In particular this is the casefor the infinity of the natural numbers. Therefore statements thatquantify over this set have to be treated with caution. On the otherhand, the principle of induction is fully acceptable from anintuitionistic point of view.

Because of the finiteness of a natural number in contrast to, forexample, a real number, many arithmetical statements of a finitenature that are true in classical mathematics are so in intuitionismas well. For example, in intuitionism every natural number has a primefactorization; there exist computably enumerable sets that are notcomputable; \((A \vee \neg A)\) holds for all quantifier freestatements \(A\). For more complex statements, such as van derWaerden’s theorem or Kruskal’s theorem, intuitionisticvalidity is not so straightforward. In fact, the intuitionistic proofsof both statements are complex and deviate from the classical proofs(Coquand 1995, Veldman 2004).

Thus in the context of the natural numbers, intuitionism and classicalmathematics have a lot in common. It is only when other infinite setssuch as the real numbers are considered that intuitionism starts todiffer more dramatically from classical mathematics, and from mostother forms of constructivism as well.

3.4 The continuum

In intuitionism, the continuum is both an extension and a restrictionof its classical counterpart. In its full form, both notions areincomparable since the intuitionistic real numbers possess propertiesthat the classical real numbers do not have. A famous example, to bediscussed below, is the theorem that in intuitionism every totalfunction on the continuum is continuous. That the intuitionisticcontinuum does not satisfy certain classical properties can be easilyseen viaweak counterexamples. That it also containsproperties that the classical reals do not posses stems from theexistence, in intuitionism, ofchoice sequences.

Weak counterexamples

Theweak counterexamples, introduced by Brouwer in 1908, arethe first examples that Brouwer used to show that the shift from aclassical to an intuitionistic conception of mathematics is notwithout consequence for the mathematical truths that can beestablished according to these philosophies. They show that certainclassical statements are presently unacceptable from an intuitionisticpoint of view. As an example, consider the sequence of real numbersgiven by the following definition:

Here \(A(n)\) is a decidable property for which \(\forall n A(n)\) isnot known to be true or false. Decidability means that at present forany given \(n\) there exists (can be constructed) a proof of \(A(n)\)or of \(\neg A(n)\). At the time of this writing, we could for examplelet \(A(n)\) express that \(n\), if greater than 2, is the sum ofthree primes; \(\forall n A(n)\) then expresses the (original)Goldbach conjecture that every number greater than 2 is the sum ofthree primes. The sequence \(\langle r_n \rangle\) defines a realnumber \(r\) for which the statement \(r=0\) is equivalent to thestatement \(\forall n A(n)\). It follows that the statement \((r = 0\vee r \neq 0)\) does not hold, and therefore that the law oftrichotomy \(\forall x(x \lt y \vee x=y \vee x \gt y)\) is not true onthe intuitionistic continuum.

Note the subtle difference between “\(A\) is notintuitionistically true ” and “\(A\) is intuitionisticallyrefutable”: in the first case we know that \(A\) cannot have anintuitionistic proof, the second statement expresses that we have aproof of ¬A, i.e. a construction that derives falsum fromany possible proof of \(A\). For the law of trichotomy we have justshown that it is not intuitionistically true. Below it will be shownthat even the second stronger form saying that the law is refutableholds intuitionistically. This, however, is not true for allstatements for which there exist weak counterexamples. For example,the Goldbach conjecture is a weak counterexample to the principle ofthe excluded middle, since \(\forall n A(n)\) as above is at presentnot known to be true or false, and thus we cannot assert \(\forall nA(n) \vee \neg \forall n A(n)\) intuitionistically, at least not atthis moment. But the refutation of this statement, \(\neg (\forall nA(n) \vee \neg \forall n A(n))\), is not true in intuitionism, as onecan show that for any statement \(B\) a contradiction can be derivedfrom the assumption that \(\neg B\) and \(\neg\neg B\) hold (and thusalso from \(B\) and \(\neg B\)). In other words, \(\neg\neg (B \vee\neg B)\) is intuitionistically true, and thus, although there existweak counterexamples to the principle of the excluded middle, itsnegation is false in intuitionism, that is, it is intuitionisticallyrefutable.

The existence of real numbers \(r\) for which the intuitionist cannotdecide whether they are positive or not shows that certain classicallytotal functions cease to be so in an intuitionistic setting, such asthe piecewise constant function

There exist weak counterexamples to many classically valid statements.The construction of these weak counterexamples often follow the samepattern as the example above. For example, the argument that showsthat the intermediate value theorem is not intuitionistically validruns as follows. Let \(r\) be a real number in [−1,1] for which\((r\leq 0 \vee 0 \lt r)\) has not been decided, as in the exampleabove. Define the uniformly continuous function \(f\) on \([0,3]\)by

Clearly, \(f(0) = -1 +r\) and \(f(3) = 1 + r\), whence \(f\) takes thevalue 0 at some point \(x\) in [0,3]. If such \(x\) could bedetermined, either \(1 \leq x\) or \(x \leq 2\). Since \(f\) equals\(r\) on \([1,2]\), in the first case \(r \leq 0\) and in the secondcase \(0\leq r\), contradicting the undecidability of the statement\((r\leq 0 \vee 0 \leq r)\).

These examples seem to indicate that in the shift from classical tointuitionistic mathematics one loses several fundamental theorems ofanalysis. This however is not so, since in many cases intuitionismregains such theorems in the form of an analogue in which existentialstatements are replaced by statements about the existence ofapproximations within arbitrary precision, as in this classicallyequivalent form of the intermediate value theorem that isconstructively valid:

Theorem. For every continuous real-valued function\(f\) on an interval \([a,b]\) with \(a \lt b\), for every \(c\)between \(f(a)\) and \(f(b)\), the following holds:

\[ \forall n \exists x \in [a,b] \, |f(x)-c| \lt 2^{-n}.\]

Weak counterexamples are a means to show that certain mathematicalstatements do not hold intuitionistically, but they do not yet revealthe richness of the intuitionistic continuum. Only afterBrouwer’s introduction of choice sequences did intuitionismobtain its particular flavor and became incomparable with classicalmathematics.

Choice sequences

Choice sequences were introduced by Brouwer to capture theintuition of the continuum. Since for the intuitionist all infinity ispotential, infinite objects can only be grasped via a process thatgenerates them step-by-step. What will be allowed as a legitimateconstruction therefore decides which infinite objects are to beaccepted. For example, in most other forms of constructivism onlycomputable rules for generating such objects are allowed, while inPlatonism infinities are considered to be completed totalities whoseexistence is accepted even in cases when no generating rules areknown.

Brouwer’s second act of intuitionism gives rise to choicesequences, that provide certain infinite sets with properties that areunacceptable from a classical point of view. A choice sequence is aninfinite sequence of numbers (or finite objects) created by the freewill. The sequence could be determined by a law or algorithm, such asthe sequence consisting of only zeros, or of the prime numbers inincreasing order, in which case we speak of alawlikesequence, or it could not be subject to any law, in which case it iscalledlawless. Lawless sequences could for example becreated by the repeated throw of a coin, or by asking the CreatingSubject to choose the successive numbers of the sequence one by one,allowing it to choose any number to its liking. Thus a lawlesssequence is ever unfinished, and the only available information aboutit at any stage in time is the initial segment of the sequence createdthus far. Clearly, by the very nature of lawlessness we can neverdecide whether its values will coincide with a sequence that islawlike. Also, the free will is able to create sequences that startout as lawlike, but for which at a certain point the law might belifted and the process of free choice takes over to generate thesucceeding numbers, or vice versa.

According to Brouwer every real number is represented by a choicesequence, and the choice sequences enabled him to capture theintuitionistic continuum via the controversial continuity axioms.Brouwer first spoke of choice sequences in his inaugural address(Brouwer 1912), but at that time he did not yet treat them as afundamental part of his mathematics. Gradually they became moreimportant and from 1918 on Brouwer started to use them in a wayexplained in the next section.

3.5 Continuity axioms

The acceptance of the notion of choice sequence has far-reachingimplications. It justifies, for the intuitionist, the use of thecontinuity axioms, from which classically invalid statements can bederived. The weakest of these axioms is the weak continuity axiom:

Here \(n\) and \(m\) range over natural numbers, \(\alpha\) and\(\beta\) over choice sequences, and \(\beta\in\alpha(\overline{m})\)means that the first \(m\) elements of \(\alpha\) and \(\beta\) areequal. Although until now there has never been given a completelysatisfactory justification of most continuity axioms for arbitrarychoice sequences, not even by Brouwer, when restricted to the class oflawless sequences arguments supporting the validity of the weakcontinuity axiom run as follows. When could a statement of the form\(\forall\alpha\exists n A(\alpha,n)\) be established by theintuitionist? By the very nature of the notion of lawless sequence,the choice of the number \(n\) for which \(A(\alpha,n)\) holds has tobe made after only a finite initial segment of \(\alpha\) is known.For we do not know how \(\alpha\) will proceed in time, and wetherefore have to base the choice of \(n\) on the initial segment of\(\alpha\) that is known at that point in time where we wish to fix\(n\). This implies that for every lawless sequence \(\beta\) with thesame initial segment as \(\alpha\), \(A(\beta,n)\) holds as well.

The weak continuity axiom has been shown to be consistent, and isoften applied in a form that can be justified, namely in the case inwhich the predicate \(A\) only refers to the values of \(\alpha\), andnot to the higher order properties that it possibly possesses. Thedetails of the argument will be omitted here, but it contains the sameingredients as the justification of the principle for lawlesssequences, and can be found in van Atten and van Dalen 2002.

Weak continuity does not exhaust the intuitionists’ intuitionabout the continuum, for given the weak continuity axiom, it seemsreasonable to assume that the choice of the number \(m\) such that\(\forall\beta\in\alpha(\overline{m})A(\beta,n)\), could be madeexplicit. Thus \(\forall\alpha\exists n A(\alpha,n)\) implies theexistence of a continuous functional \(\Phi\) that for every\(\alpha\) produces the \(m\) that fixes the length of \(\alpha\) onthe basis of which \(n\) is chosen. More formally, let\(\mathcal{CF}\) be the class of continuous functionals \(\Phi\) thatassign natural numbers to infinite sequences, i.e. that satisfy

The full axiom of continuity, which is an extension of the weakcontinuity axiom, can then be expressed as:

Through the continuity axiom certain weak counterexamples can betransformed into genuine refutations of classically acceptedprinciples. For example, it implies that the quantified version of theprinciple of the excluded middle is false:

Here \(\alpha(n)\) denotes the \(n\)-th element of \(\alpha\). To seethat this negations holds, suppose, arguing by contradiction, that\(\neg\forall\alpha(\forall n\alpha (n)=0 \vee \neg \forall n\alpha(n)=0)\) holds. This implies that

By the weak continuity axiom, for \(\alpha\) consisting of only zerosthere exists a number \(m\) that fixes the choice of \(k\), whichmeans that for all \(\beta\in\alpha(\overline{m})\), \(k=0\). But theexistence of sequences whose first \(m\) elements are 0 and thatcontain a 1 show that this cannot be.

This example showing that the principle of the excluded middle notonly does not hold but is in fact false in intuitionism, leads to therefutation of many basic properties of the continuum. Consider forexample the real number \(r_\alpha\) that is the limit of the sequenceconsisting of the numbers \(r_n\) as given in the section on weakcounterexamples, where the \(A(m)\) in the definition is taken to bethe statement \(\alpha(m)=0\). Then the refutation above implies that\(\neg\forall\alpha(r_\alpha=0 \vee r_\alpha\neq 0)\), and it therebyrefutes the law of trichotomy:

The following theorem is another example of the way in which thecontinuity axiom refutes certain classical principles.

Theorem \({\bf (C\mbox{-}N)}\) Every total realfunction is continuous.

Indeed, a classical counterexample to this theorem, the nowherecontinuous function \[ f(x) = \begin{cases} 0 \text{ if \(x\) is a rational number } \\ 1 \text{ if \(x\) is an irrational number} \end{cases}\] is not a legitimate function from theintuitionistic point of view since the property of being rational isnot decidable on the real numbers. The theorem above implies that thecontinuum is not decomposable, and in van Dalen 1997, it is shown thatthis even holds for the set of irrational numbers.

The two examples above are characteristic for the way in which thecontinuity axioms are applied in intuitionistic mathematics. They arethe only axioms in intuitionism that contradict classical reasoning,and thereby represent the most colorful as well as the mostcontroversial part of Brouwer’s philosophy.

Neighborhood Functions

There is a convenient representation of continuous functionals thathas been used extensively in the literature, though not by Brouwerhimself. Continuous functionals that assign numbers to infinitesequences can be represented byneighborhood functions, wherea neighborhood function \(f\) is a function on the natural numberssatisfying the following two properties (\(\cdot\) denotesconcatenation and \(f(\alpha(\overline{n}))\) denotes the value of\(f\) on the code of the finite sequence\(\alpha(\overline{n})\)).

Intuitively, if \(f\) represents \(\Phi\) then\(f(\alpha(\overline{n}))=0\) means that \(\alpha(\overline{n})\) isnot long enough to compute \(\Phi(\alpha)\), and\(f(\alpha(\overline{n}))=m+1\) means that \(\alpha(\overline{n})\) islong enough to compute \(\Phi(\alpha)\) and that the value of\(\Phi(\alpha)\) is \(m\). If \(\mathcal{K}\) denotes the class ofneighborhood functions, then the continuity axiom \({\bf C\mbox{-}N}\)can be rephrased as \[ \forall \alpha\exists n A(\alpha,n) \rightarrow \exists f \in \mathcal{K}\, \forall m(f(m) \gt 0 \rightarrow \forall \beta \in m A(\beta,f(m-1))), \]

where \(\beta \in m\) means that the code of the initial segment of\(\beta\) is \(m\).

3.6 The bar theorem

Brouwer introduced choice sequences and the continuity axioms tocapture the intuitionistic continuum, but these principles alone donot suffice to recover that part of traditional analysis that Brouwerconsidered intuitionistically sound, such as the theorem that everycontinuous real function on a closed interval is uniformly continuous.For this reason Brouwer proved the so-called bar theorem. It is aclassically valid statement, but the proof Brouwer gave is by manyconsidered to be no proof at all since it uses an assumption on theform of proofs for which no rigorous argument is provided. This is thereason that the bar theorem is also referred to as the bar principle.

The most famous consequence of the bar theorem is the fan theorem,which suffices to prove the aforementioned theorem on uniformcontinuity, and which will be treated first. Both the fan and the bartheorem allow the intuitionist to use induction along certainwell-founded sets of objects called spreads. Aspread is theintuitionistic analogue of a set, and captures the idea of infiniteobjects as ever growing and never finished. A spread is essentially acountably branching tree labelled with natural numbers or other finiteobjects and containing only infinite paths.

Afan is a finitely branching spread, and the fan principleexpresses a form of compactness that is classically equivalent toKönig’s lemma, the classical proof of which is unacceptablefrom the intuitionistic point of view. The principle states that forevery fan \(T\) in which every branch at some point satisfies aproperty \(A\), there is a uniform bound on the depth at which thisproperty is met. Such a property is called abar for\(T\).

Here \(\alpha \in T\) means that \(\alpha\) is a branch of \(T\). TheprincipleFAN suffices to prove the theorem mentionedabove:

Theorem (FAN) Every continuous realfunction on a closed interval is uniformly continuous.

Brouwer’s justification for the fan theorem is his bar principlefor the universal spread:

Here \(\varepsilon\) stands for the empty sequence, \(\cdot\) forconcatenation,BI for Bar Induction, and thesubscriptD refers to the decidability of thepredicate \(A\). The bar principle provides intuitionism with aninduction principle for trees; it expresses a well-foundednessprinciple for spreads with respect to decidable properties. Extensionsof this principle in which the decidability requirement is weakenedcan be extracted from Brouwer’s work but will be omitted here.Continuity and the bar principle are sometimes captured in one axiomcalled thebar continuity axiom.

There is a close connection between the bar principle and theneighborhood functions mentioned in the section on continuity axioms.Let \(\mathcal{IK}\) be the inductively defined class of neighborhoodfunctions, consisting of all constant non-zero sequences \(\lambdam.n+1\), and such that if \(f(0)=0\) and \(\lambda m.f(x\cdot m)\in\mathcal{IK}\) for all \(x\), then \(f \in \mathcal{IK}\). Thestatement \(\mathcal{K}=\mathcal{IK}\), that is, the statement thatthe neighborhood functions can be generated inductively, is equivalenttoBI_D.

Brouwer’s proof of the bar theorem is remarkable in that it useswell-ordering properties ofhypothetical proofs. It is basedon the assumption that any proof that a propertyA onsequences is a bar can be decomposed into acanonical proofthat is well-ordered. Although it is classically valid,Brouwer’s proof of the principle shows that the reason foraccepting it as a valid principle in intuitionism differsfundamentally from the argument supporting its acceptability inclassical mathematics.

3.7 Choice axioms

The axiom of choice in its full form is unacceptable from aconstructive point of view, at least in the presence of certain othercentral axioms of set theory, such as extensionality (Diaconescu1975). For let \(A\) be a statement that is not known to be true orfalse. Then membership of the following two sets is undecidable.

The existence of a choice function \(f:\{X,Y\} \rightarrow \{0,1\}\)choosing an element from \(X\) and \(Y\) would imply \((A \vee \negA)\). For if \(f(X)\neq f(Y)\), it follows that \(X\neq Y\), and hence\(\neg A\), whereas \(f(X)=f(Y)\) implies \(A\). Therefore a choicefunction for \(\{X,Y\}\) cannot exist.

There are, however, certain restrictions of the axiom that areacceptable for the intuitionist, for example theaxiom ofcountable choice, also accepted as a legitimate principle by thesemi-intuitionists to be discussed below:

This scheme may be justified as follows. A proof of the premise shouldprovide a method that given \(m\) provides a number \(n\) such that\(mRn\). Thus the function \(\alpha\) on the natural numbers\(\mathbb{N}\) can be constructed step-by-step: first an element\(m_0\) is chosen such that \(0Rm_0\), which will be the value of\(\alpha(0)\). Then an element \(m_1\) is chosen such that \(1Rm_1\),which will be the value of \(\alpha(1)\), and so on.

Several other choice axioms can be justified in a similar way. Onlyone more will be mentioned here, the axiom of dependent choice:

Also in classical mathematics the choice axioms are treated with care,and it is often explicitly mentioned how much choice is needed in aproof. Since the axiom of dependent choice is consistent with animportant axiom in classical set theory (the axiom of determinacy)while the full axiom of choice is not, special attention is payed tothis axiom and in general one tries to reduce the amount of choice ina proof, if choice is present at all, to dependent choice.

3.8 Descriptive set theory, topology, and topos theory

Brouwer was not alone in his doubts concerning certain classical formsof reasoning. This is particularly visible in descriptive set theory,which emerged as a reaction to the highly nonconstructive notionsoccurring in Cantorian set theory. The founding fathers of the field,including Émile Borel and Henri Lebesgue as two of the mainfigures, were calledsemi-intuitionists, and theirconstructive treatment of the continuum led to the definition of theBorel hierarchy. From their point of view a notion like the set of allsets of real numbers is meaningless, and therefore has to be replacedby a hierarchy of subsets that do have a clear description.

In Veldman 1999, an intuitionistic equivalent of the notion of Borelset is formulated, and it is shown that classically equivalentdefinitions of the Borel sets give rise to a variety ofintuitionistically distinct classes, a situation that often occurs inintuitionism. For the intuitionistic Borel sets an analogue of theBorel Hierarchy Theorem is intuitionistically valid. The proof of thisfact makes essential use of the continuity axioms discussed above andthereby shows how classical mathematics can guide the search forintuitionistic analogues that, however, have to be proved in acompletely different way, sometimes using principles unacceptable froma classical point of view.

Another approach to the study of subsets of the continuum, or of atopological space in general, has appeared through the development offormal or abstract topology (Fourman 1982, Martin-Löf 1970,Sambin 1987). In this constructive topology the role of open sets andpoints is reversed; in classical topology an open set is defined as acertain set of points, in the constructive case open sets are thefundamental notion and points are defined in terms of them. Thereforethis approach is sometimes referred to as point-free topology.

Intuitionistic functional analysis has been developed far and wide bymany after Brouwer, but since most approaches are not strictlyintuitionistic but also constructive in the wider sense, this researchwill not be addressed any further here.

4. Constructivism

Intuitionism shares a core part with most other forms ofconstructivism. Constructivism in general is concerned withconstructive mathematical objects and reasoning. From constructiveproofs one can, at least in principle, extract algorithms that computethe elements and simulate the constructions whose existence isestablished in the proof. Most forms of constructivism are compatiblewith classical mathematics, as they are in general based on a stricterinterpretation of the quantifiers and the connectives and theconstructions that are allowed, while no additional assumptions aremade. The logic accepted by almost all constructive communities is thesame, namely intuitionistic logic.

Many existential theorems in classical mathematics have a constructiveanalogue in which the existential statement is replaced by a statementabout approximations. We saw an example of this, the intermediatevalue theorem, in the section on weak counterexamples above. Largeparts of mathematics can be recovered constructively in a similar way.The reason not to treat them any further here is that the focus inthis entry is on those aspects of intuitionism that set it apart fromother constructive branches of mathematics. For a thorough treatmentof constructivism the reader is referred to the corresponding entry inthis encyclopedia.

5. Meta-mathematics

Although Brouwer developed his mathematics in a precise andfundamental way, formalization in the sense as we know it today wasonly carried out later by others. Indeed, according to Brouwer’sview that mathematics unfolds itself internally, formalization,although not unacceptable, is unnecessary. Others after him thoughtotherwise, and the formalization of intuitionistic mathematics and thestudy of its meta-mathematical properties, in particular of arithmeticand analysis, have attracted many researchers. The formalization ofintuitionistic logic on which all formalizations are based has alreadybeen treated above.

5.1 Arithmetic

Heyting ArithmeticHA as formulated by Arend Heytingis a formalization of the intuitionistic theory of the natural numbers(Heyting 1956). It has the same non-logical axioms as Peano ArithmeticPA but it is based on intuitionistic logic. Thus itis a restriction of classical arithmetic, and it is the acceptedtheory of the natural numbers in almost all areas of constructivemathematics. Heyting Arithmetic has many properties that reflect itsconstructive character, for example the Disjunction Property thatholds for intuitionistic logic too. Another property ofHA thatPA does not share is thenumerical existence property: (\(\overline{n}\) is the numeralcorresponding to natural number \(n\))

That this property does not hold inPA follows fromthe fact thatPA proves \(\exists x (A(x) \vee\forall y \neg A(y))\). Consider, for example, the case that \(A(x)\)is the formula \(T(e,e,x)\), where \(T\) is the decidable Kleenepredicate expressing that \(x\) is the code of a terminatingcomputation of the program with code \(e\) on input \(e\). If forevery \(e\) there would exist a number \(n\) such that \({\bfPA}\vdash T(e,e,n) \vee \forall y \neg T(e,e,y)\), then by checkingwhether \(T(e,e,n)\) holds it would be decided whether a program \(e\)terminates on input \(e\). This, however, is in general undecidable.

Markov’s rule is a principle that holds both classically andintuitionistically, but only forHA the proof of thisfact is nontrivial:

SinceHA proves the law of the excluded middle forevery primitive recursive predicate, it follows that for such \(A\)the derivability of \(\neg\neg \exists x A(x)\) inHAimplies the derivability of \(\exists x A(x)\) as well. From this itfollows thatPA is \(\Pi^0_2\)-conservative overHA. That is, for primitive recursive \(A\):\[ {\bf PA} \vdash \forall x \exists y A(x,y) \Rightarrow {\bf HA} \vdash \forall x \exists y A(x,y).\] Thus the class of provably recursive functions ofHA coincides with the class of provably recursivefunctions ofPA, a property that, on the basis of theideas underlying constructivism and intuitionism, may not come as asurprise.

5.2 Analysis

The formalization of intuitionistic mathematics covers more thanarithmetic. Large parts of analysis have been axiomatized from aconstructive point of view (Kleene 1965, Troelstra 1973). Theconstructivity of these systems can be established using functional,type theoretic, or realizability interpretations, most of them basedon or extensions of Gödel’s Dialectica interpretation(Gödel 1958, Kreisel 1959), Kleene realizability (Kleene 1965),or type theories (Martin-Löf 1984). In these interpretations thefunctionals underlying constructive statements, such as for examplethe function assigning a \(y\) to every \(x\) in \(\forall x\exists yA(x,y)\), are made explicit in various ways.

In (Scott 1968 and 1970), a topological model for the second-orderintuitionistic theory of analysis is presented where the reals areinterpreted as continuous functions from Baire space into theclassical reals. In this model Kripke’s Schema as well ascertain continuity axioms hold. In (Moschovakis 1973), this method isadapted to construct a model of theories of intuitionistic analysis interms of choice sequences. Also in this model Kripke’s Schemaand certain continuity axioms hold. In (Van Dalen 1978) Beth modelsare used to provide a model of arithmetic and choice sequences thatsatisfy choice schemata, instances of weak continuity andKripke’s Schema. In this model the domains at every node are thenatural numbers, so that one does not have to use nonstandard models,as in the case of Kripke models. Moreover, the axiomsCS1–3 of the creating subject can beinterpreted in it, thus showing this theory to be consistent.

5.3 Lawless sequences

There exist axiomatizations of the lawless sequences, and they allcontain extensions of the continuity axioms (Kreisel 1968, Troelstra1977). In particular in the form of the Axiom of Open Data statingthat for \(A(\alpha)\) not containing other nonlawlike parametersbesides \(\alpha\):

In (Troelstra 1977), a theory of lawless sequences is developed (andjustified) in the context of intuitionistic analysis. Besides axiomsfor elementary analysis it contains, for lawless sequences,strengthened forms of the axioms of open data, continuity,decidability and density (density says that every finite sequence isthe initial segment of a lawless sequence). What is especiallyinteresting is that in these theories quantifiers over lawlesssequences can be eliminated, a result that can also be viewed asproviding a model of lawlike sequences for such theories. Otherclassical models of the theory of lawless sequences have beenconstructed in category theory in the form of sheaf models (van derHoeven and Moerdijk 1984). In (Moschovakis 1986), a theory for choicesequences relative to a certain set of lawlike elements is introduced,along with a classical model in which the lawless sequences turn outto be exactly the generic ones.

5.4 Formalization of the Creating Subject

The Creating Subject, introduced in Section 2.2, can generate choicesequences, which are some of the most important and complicatedmathematical entities of Brouwer’s Intuitionism. Severalphilosophers and mathematicians have tried to develop the theory ofthe Creating Subject further mathematically as well asphilosophically.

In the formalization of the notion of the Creating Subject itstemporal aspect is formalized using the notation \(\Box_n A\), thatdenotes that the Creating Subject has a proof of A at time n (in someother formulations: experiences the truth of \(A\) at time \(n\)).Georg Kreisel (1967) introduced the following three axioms for theCreating Subject, which taken together are denoted byCS:

In the version of Anne Troelstra (1969) the last axiom is strengthenedto

The first axiomCS1 is uncontroversial: at any point in time,it can be established whether the Creating Subject has a proof of agiven statement or not. The second axiomCS2 clearly uses thefact that the Creating Subject is an idealization since it expressesthat proofs will always be remembered. The last axiomCS3 isthe most disputed part of the formalization of the Creating Subject,or better, its second conjunct \((A \rightarrow \neg\neg\exists n\Box_n A)\)is, which was given the nameAxiom of Christian Charity byKreisel. Göran Sundholm (2014), for example, argues that Axiom ofChristian Charity is not acceptable from a constructive point of view.And Gödel’s incompleteness theorem even implies that theprinciple is false when \(\Box_n A\) would be interpreted as beingprovable in a sufficiently strong proof system, which, however, iscertainly not the interpretation that Brouwer had in mind.

Given a statement \(A\) that does not contain any reference to time,i.e. no occurrence of \(\Box_n\), one can define a choice sequenceaccording to the following rule (Brouwer 1953):

From this follows the principle known as Kripke’s SchemaKS, introduced in Section 2.2, a principle that unlike theaxioms of the theory of the Creating Subject, contains no explicitreference to time: \(\exists \alpha (A \leftrightarrow \exists n\alpha(n) = 1)\).

Using Kripke’s Schema, the weak counter example arguments can beexpressed formally without any reference to the Creating Subject. Thefollowing example is taken from (van Atten 2018). Let A be a statementfor which at present \(\neg A \vee \neg\neg A\) is not known to hold.UsingKS one obtains choice sequences \(\alpha_1\) and\(\alpha_2\) such that

Associate with these two sequences the real numbers \(r_0\) and\(r_1\), where for \(i=0,1\):

Then for \(r=r_0 + r_1\), statement \(\neg A \vee \neg\neg A\) isimplied by \((r\gt 0\vee r\lt 0)\), which shows that \((r\gt 0\veer\lt 0)\) cannot be proved.

In (van Dalen 1978) a model is constructed of the axioms for theCreating Subject in the context of arithmetic and choice sequences,thus proving them to be consistent with intuitionistic arithmetic andcertain parts of analysis. In (van Dalen 1982),CS is proven tobe conservative over Heyting Arithmetic. Mathematical consequences ofKripke’s Schema can be found in (van Dalen 1997), where it isshown thatKS and the continuity axioms reject Markov’sprinciple, whileKS together with Markov’s principleimplies the principle of the excluded middle.

Kripke has shown thatKS implies the existence of nonrecursivefunctions, a result not published by him but by Kreisel (1970).Clearly, this implies that the theoryCS also implies theexistence of a nonrecursive function. A possible argument forCS runs as follows. Suppose \(X\) is a noncomputable butcomputably enumerable set and define the function \(f\) asfollows:

Then it follows that \(n\not\in X\) if and only if \(f(m,n)=1\) forsome natural number \(m\), which implies that \(f\) cannot becomputable. For if so, the complement of \(X\) would be computablyenumerable, implying the computability of \(X\). Since \(f\) is afunction from the intuitionistic point of view, this establishes thatin Intuitionism not all functions are computable.

5.5 Foundations

Formalizations that are meant to serve as a foundation forconstructive mathematics are either of a set-theoretic (Aczel 1978,Myhill 1975) or type-theoretic (Martin-Löf 1984) nature. Theformer theories are adaptations of Zermelo-Fraenkel set theory to aconstructive setting, while in type theory the constructions implicitin constructive statements are made explicit in the system. Set theorycould be viewed as an extensional foundation of mathematics whereastype theory is in general an intensional one.

In recent years many models of parts of such foundational theories forintuitionistic mathematics have appeared, some of them have beenmentioned above. Especially in topos theory (van Oosten 2008) thereare many models that capture certain characteristics of intuitionism.There are, for example, topoi in which all total real functions arecontinuous. Functional interpretations such as realizability as wellas interpretations in type theory could also be viewed as models ofintuitionistic mathematics and most other constructive theories.

5.6 Reverse mathematics

In reverse mathematics one tries to establish for mathematicaltheorems which axioms are needed to prove them. In intuitionisticreverse mathematics one has a similar aim, but then with respect tointuitionistic theorems: working over a weak intuitionistic theory,axioms and theorems are compared to each other. The typical axiomswith which one wishes theorems to compare are the fan principle andthe bar principle, Kripke’s schema and the continuityaxioms.

In (Veldman 2011), equivalents of the fan principle over a basictheory called Basic Intuitionistic Mathematics are studied. It isshown that the fan principle is equivalent to the statement that theunit interval [0,1] has the Heine-Borel property, and from this manyother equivalents are derived. In (Veldman 2009), the fan principle isshown to also be equivalent to Brouwer’s Approximate Fixed-PointTheorem. In (Lubarsky et al. 2012), reverse mathematics is applied toa form of Kripke’s schema, which is shown to be equivalent tocertain topological statements.

There are many more of such examples from intuitionistic reversemathematics. Especially in the larger field of constructive reversemathematics there are many results of this nature that are alsorelevant from the intuitionistic point of view.

6. Philosophy

Brouwer build his Intuitionism from the ground up and didnot comment much on the relation between Intuitionism and otherexisting philosophies, but others after him did. Some of theseconnections are discussed in this section, in particular the way inwhich intuitionistic principles can be justified in terms of otherphilosophies.

6.1 Phenomenology

The connection between Intuitionism and Phenomenology, the philosophydeveloped by Edmund Husserl, has been investigated by several authors,during Brouwer’s lifetime as well as decades later. Hermann Weylwas among the first to discuss the relation between Brouwer’sideas and the phenomenological view on mathematics. Like Brouwer, Weylspeaks in his bookDas Kontinuum (Chapter 2) about theintuitive continuum, but Weyl’s notion is based on thephenomenology of (the consciousness of) time. Weyl later feels thatBrouwer’s development of real analysis is more faithful to theidea of the intuitive continuum than his own (Weyl 1921) and thereforeplaces himself at Brouwer’s side, at least regarding this aspect(van Atten 2002).

Van Atten (2003 en 2007) uses phenomenology to justify choicesequences as mathematical objects. The author (2002) is critical aboutBrouwer’s justification of choice sequences, which is the motiveto look for a philosophical justification elsewhere. Choice sequencesoccur in the work of Becker (1927) and Weyl, but they differ fromBrouwer’s notion, and Husserl never discussed choice sequencespublicly. Van Atten explains how thehomogeneity of thecontinuum accounts for its inexhaustibility and nonatomicity, two keyproperties of the intuitive continuum according to Brouwer. Using thefact that these two essential properties are present in the definitionof choice sequences, one arrives at a phenomenological justificationof them.

6.2 Wittgenstein

On March 10, 1928, Brouwer lectured in Vienna on his intuitionisticfoundations of mathematics. Ludwig Wittgenstein attended that lecture,persuaded by Herbert Feigl, who afterwards wrote about the hours hespent with Wittgenstein and others after the lecture:a greatevent took place. Suddenly and very volubly Wittgenstein began talkingphilosophy – at great length. Perhaps this was the turningpoint, for ever since that time, 1929, when he moved to CambridgeUniversity, Wittgenstein was a philosopher again, and began to exert atremendous influence.

Others dispute that Brouwer’s lecture influencedWittgenstein’s thinking (Hacker 1986, Hintikka 1992, Marion2003). In how far, if at all, Wittgenstein was influenced byBrouwer’s ideas is not entirely clear, but there certainly areinteresting agreements and disagreements between their views. Marion(2003) argues that Wittgenstein’s conception of mathematics asdescribed in the Tractatus is very close to that of Brouwer, and thatWittgenstein agrees with the rejection of the Law of Excluded Middle(1929 manuscript, pp 155–156 in Wittgenstein 1994) but disagreeswith Brouwer’s arguments against it. Marion (2003) claims thatWittgenstein’s stance is more radical than Brouwer’s inthat in the former’s view the lack of validity of the Law ofExcluded Middle in mathematics is a distinguishing feature of allmathematical propositions (as opposed to empirical propositions) andnot only a particularity of the mathematics of the infinite, as it isfor Brouwer.

Veldman (forthcoming) discusses several points of (dis)agreement betweenBrouwer and Wittgenstein, such as the danger of logic, which,according to both, may lead to constructions without mathematicalcontent. One of the disagreements raised in the paper concernsWittgenstein’s view that mathematics is a common undertaking,which is in stark contrast to Brouwer’s Creating Subject and hisview that mathematics is a languageless activity.

6.3 Dummett

The British philosopher Michael Dummett (1975) developed aphilosophical basis for Intuitionism, in particular for intuitionisticlogic. Dummett explicitly states that his theory is not an exegesis ofBrouwer’s work, but a possible philosophical theory for (in hiswords)repudiating classical reasoning in mathematics in favor ofintuitionistic reasoning.

Dummett’s approach starts with the idea that the choice for onelogic over another must necessarily lie in the meaning one attaches tological statements. In the theory of meaning that Dummett uses, whichis based on Wittgenstein’s ideas about language and inparticular on his idea thatmeaning is use, the meaning of asentence is determined by the way in which the sentence is used. Themeaning of a mathematical statement manifests itself in the use madeof it, and theunderstanding of it is the knowledge of thecapacity to use the statement. This view is supported by the way inwhich we acquire mathematical knowledge. When we learn a mathematicalnotion we learn how to use it: how to compute it, prove it or inferfrom it. And the only way to establish that we have grasped themeaning of a mathematical statement lies in our proficiency in makingcorrect use of the statement.

Given this view on meaning, the central notion in the theory ofmeaning for mathematics is not, as in Platonism, truth, butproof; the understanding of a mathematical statement consistsin the ability to recognize a proof of it when one is presented withone. This then, as Dummett argues, leads to the adoption ofintuitionistic logic as the logic of mathematical reasoning.

Interestingly, as Dummett (1975) remarks himself, his theory ofmeaning is far apart from Brouwer’s ideas on mathematics as anessentially languageless activity. So that there are at least twoquite different lines of thought that lead to the adoption ofintuitionistic logic over classical logic, the one developed byBrouwer and the one argued for by Dummett. Dummett’s work onIntuitionism has been commented on by various philosophers such as DagPrawitz (1977), Parsons (1986) and Richard Tieszen (1994 en 2000).

6.4 Finitism

Various forms ofFinitism are based on a similar view as theone expressed by Dummett, but in which the constructions that areallowed to prove mathematical statements are required to exist notonly in principle, but also in practice. Depending on the preciseimplementation of the latter notion one arrives at different forms ofFinitism, such as theUltra-Intuitionism developed byAlexander Yessenin-Volpin (1970) and theStrict Finitismdeveloped by Crispin Wright (1982).

Bibliography

• Aczel, P., 1978, ‘The type-theoretic interpretation ofconstructive set theory,’ in A. Macintyre, L. Pacholski,J. Paris (eds.),Logic Colloquium ’77, special issueofStudies in Logic and the Foundations of Mathematics, 96:55–66.
• van Atten, M., 2004,On Brouwer, Belmont:Wadsworth/Thomson Learning.
• –––, 2007,Brouwer meets Husserl: On thephenomenology of choice sequences, Dordrecht: Springer.
• –––, 2008, ‘On the hypothetical judgementin the history of intuitionistic logic,’ in C. Glymour andW. Wang and D. Westerståhl (eds.),Proceedings of the 2007International Congress in Beijing (Logic, Methodology, andPhilosophy of Science: Volume XIII), London: King’s CollegePublications, 122–136.
• van Atten, M. and D. van Dalen, 2002, ‘Arguments for thecontinuity principle,’Bulletin of Symbolic Logic,8(3): 329–374.
• Beth, E.W., 1956, ‘Semantic construction of intuitionisticlogic,’Mededeelingen der Koninklijke Nederlandsche Akademievan Wetenschappen,Afdeeling Letterkunde (Nieuwe Serie),19(11): 357–388.
• Brouwer, L.E.J., 1975,Collected works I, A. Heyting(ed.), Amsterdam: North-Holland.
• –––, 1976,Collected works II, H.Freudenthal (ed.), Amsterdam: North-Holland.
• –––, 1905,Leven, kunst en mystiek,Delft: Waltman.
• –––, 1907,Over de grondslagen derwiskunde, Ph.D. Thesis, University of Amsterdam, Department ofPhysics and Mathematics.
• –––, 1912, ‘Intuïtionisme enformalisme’, Inaugural address at the University of Amsterdam,1912. Also inWiskundig tijdschrift, 9, 1913.
• –––, 1925, ‘Zur Begründung derintuitionistischen Mathematik I,’MathematischeAnnalen, 93: 244–257.
• –––, 1925, ‘Zur Begründung derintuitionistischen Mathematik II,’MathematischeAnnalen, 95: 453–472.
• –––, 1948, ‘Essentially negativeproperties’,Indagationes Mathematicae, 10:322–323.
• –––, 1952, ‘Historical background,principles and methods of intuitionism,’South AfricanJournal of Science, 49 (October-November): 139–146.
• –––, 1953, ‘Points and Spaces,’Canadian Journal of Mathematics, 6: 1–17.
• –––, 1981,Brouwer’s Cambridgelectures on intuitionism, D. van Dalen (ed.), Cambridge:Cambridge University Press, Cambridge.
• –––, 1992,Intuitionismus, D. van Dalen(ed.), Mannhein: Wissenschaftsverlag.
• Brouwer, L.E.J. and C.S. Adama van Scheltema, 1984,Droevesnaar, vriend van mij – Brieven, D. van Dalen (ed.),Amsterdam: Uitgeverij de Arbeiderspers.
• Coquand, T., 1995, ‘A constructive topological proof of vander Waerden’s theorem,’Journal of Pure and AppliedAlgebra, 105: 251–259.
• van Dalen, D., 1978, ‘An interpretation of intuitionisticanalysis’,Annals of Mathematical Logic, 13:1–43.
• –––, 1997, ‘How connected is theintuitionistic continuum?,’Journal of Symbolic Logic,62(4): 1147–1150.
• –––, 1999/2005,Mystic, geometer andintuitionist, Volumes I (1999) and II (2005), Oxford: ClarendonPress.
• –––, 2001,L.E.J. Brouwer (eenbiografie), Amsterdam: Uitgeverij Bert Bakker.
• –––, 2004, ‘Kolmogorov and Brouwer onconstructive implication and the Ex Falso rule’Russian MathSurveys, 59: 247–257.
• van Dalen, D. (ed.), 2001,L.E.J. Brouwer en de grondslagenvan de wiskunde, Utrecht: Epsilon Uitgaven.
• Diaconescu, R., 1975, ‘Axiom of choice andcomplementation,’ inProceedings of the AmericanMathematical Society, 51: 176–178.
• Dummett, M., 1975, ‘The Philosophical Basis ofIntuitionistic Logic,’ in H.E. Rose and J.C. Shepherdson (eds.),Proceedings of the Logic Colloquium ’73, special issueofStudies in Logic and the Foundations of Mathematics, 80:5–40.
• Fourman, M., and R. Grayson, 1982, ‘Formal spaces,’ inA.S. Troelstra and D. van Dalen (eds.),The L.E.J. BrouwerCentenary Symposium, Amsterdam: North-Holland.
• Gentzen, G., 1934, ‘Untersuchungen über das logischeSchließen I, II,’Mathematische Zeitschrift, 39:176–210, 405–431.
• Gödel, K., 1958, ‘Über eine bisher noch nichtbenützte Erweiterung des finiten Standpunktes,’Dialectia, 12: 280–287.
• Hacker, P. M. S., 1986,Insight & Illusion. Themes in thePhilosophy of Wittgenstein, revised edition, Clarendon Press,Oxford.
• Heyting, A., 1930, ‘Die formalen Regeln derintuitionistischen Logik,’Sitzungsberichte der PreussischenAkademie von Wissenschaften. Physikalisch-mathematische Klasse,42–56.
• –––, 1956,Intuitionism, anintroduction, Amsterdam: North-Holland.
• van der Hoeven, G., and I. Moerdijk, 1984, ‘Sheaf models forchoice sequences,’Annals of Pure and Applied Logic,27: 63–107.
• Kleene, S.C., and R.E. Vesley, 1965,The foundations ofintuitionistic mathematics, Amsterdam: North-Holland.
• Kreisel, G., 1959, ‘Interpretation of analysis by means ofconstructive functionals of finite type,’ in A. Heyting(ed.),Constructivity in Mathematics, Amsterdam:North-Holland.
• –––, 1962, ‘On weak completeness ofintuitionistic predicate logic,’Journal of SymbolicLogic, 27: 139–158.
• –––, 1968, ‘Lawless sequences of naturalnumbers,’Compositio Mathematica, 20:222–248.
• Kripke, S.A., 1965, ‘Semantical analysis of intuitionisticlogic’, in J. Crossley and M. Dummett (eds.),Formalsystems and recursive functions, Amsterdam: North-Holland.
• Lubarsky, R., F. Richman, and P. Schuster 2012, ‘The Kripkeschema in metric topology’,Mathematical LogicQuarterly, 58(6): 498–501.
• Maietti, M.E., and G. Sambin, 2007, ‘Toward a minimalistfoundation for constructive mathematics,’ in L. Crosilla andP. Schuster (eds.),From sets and types to topology and analysis:toward a minimalist foundation for constructive mathematics,Oxford: Oxford University Press.
• Marion, M., 2003, ‘Wittgenstein and Brouwer’,Synthese 137: 103–127.
• Martin-Löf, P., 1970,Notes on constructivemathematics, Stockholm: Almqvist & Wiskell.
• –––, 1984,Intuitionistic type theory,Napoli: Bibliopolis.
• Moschovakis, J.R., 1973, ‘A topological interpretation ofsecond-order intuitionistic arithmetic,’CompositioMathematica, 26(3): 261–275.
• –––, 1986, ‘Relative lawlessness inintuitionistic analysis,’Journal of Symbolic Logic,52(1): 68–87.
• Myhill, J., 1975, ‘Constructive set theory,’Journal of Symbolic Logic, 40: 347–382.
• Niekus, J., 2010, ‘Brouwer’s incomplete objects’History and Philosophy of Logic, 31: 31–46.
• van Oosten, J., 2008,Realizability: An introduction to itscategorical side, (Studies in Logic and the Foundations ofMathematics: Volume 152), Amsterdam: Elsevier.
• Prawitz, D., 1977, ‘Meaning and proofs: On the conflictbetween classical and intuitionistic logic,’Theoria,43(1): 2–40.
• Parsons, C., 1986, ‘Intuition in ConstructiveMathematics,’ inLanguage, Mind and Logic, J. Butter(ed.), Cambridge: Cambridge University Press.
• Sambin, G., 1987, ‘Intuitionistic formal spaces,’ inMathematical Logic and its Applications, D. Skordev (ed.),New York: Plenum.
• Scott, D., 1968, ‘Extending the topological interpretationto intuitionistic analysis,’Compositio Mathematica,20: 194–210.
• –––, 1970, ‘Extending the topologicalinterpretation to intuitionistic analysis II’, inIntuitionism and proof theory, J. Myhill, A. Kino, and R.Vesley (eds.), Amsterdam: North-Holland.
• Sundholm, B.G., ‘Constructive Recursive Functions, Church’sThesis, and Brouwer's Theory of the Creating Subject: Afterthoughts ona Paris Joint Session’, in Jacque Dubucs & Michel Bordeau(eds.),Constructivity and Computability in Historical andPhilosophical Perspective (Logic, Epistemology, and the Unity ofScience: Volume 34), Dordrecht: Springer: 1–35.
• Tarski, A., 1938, ‘Der Aussagenkalkül und dieTopologie,’Fundamenta Mathematicae, 31:103–134.
• Tieszen, R., 1994, ‘What is the philosophical basis ofintuitionistic mathematics?,‘ in D. Prawitz, B. Skyrms andD. Westerstahl (eds.),Logic, Methodology and Philosophy ofScience, IX: 579–594.
• –––, 2000, ‘Intuitionism, Meaning Theoryand Cognition,‘History and Philosophy of Logic, 21:179–194.
• Troelstra, A.S., 1973,Metamathematical investigations ofintuitionistic arithmetic and analysis, (Lecture Notes inMathematics: Volume 344), Berlin: Springer.
• –––, 1977,Choice sequences (OxfordLogic Guides), Oxford: Clarendon Press.
• Troelstra, A.S., and D. van Dalen, 1988,Constructivism I andII, Amsterdam: North-Holland.
• Veldman, W., 1976, ‘An intuitionistic completeness theoremfor intuitionistic predicate logic,’Journal of SymbolicLogic, 41(1): 159–166.
• –––, 1999, ‘The Borel hierarchy and theprojective hierarchy in intuitionistic mathematics,’ ReportNumber 0103, Department of Mathematics, University of Nijmegen. [available online]
• –––, 2004, ‘An intuitionistic proof ofKruskal’s theorem,’Archive for MathematicalLogic, 43(2): 215–264.
• –––, 2009, ‘Brouwer’s ApproximateFixed-Point Theorem is Equivalent to Brouwer’s FanTheorem,’ in S. Lindström, E. Palmgren, K. Segerberg,V. Stoltenberg-Hansen (eds.),Logicism, Intuitionism, andFormalism (Synthese Library: Volume 341), Dordrecht: Springer,277–299.
• –––, 2014, ‘Brouwer’s Fan Theorem asan axiom and as a contrast to Kleene’s Alternative,’ inArchive for Mathematical Logic, 53(5–6):621–693.
• –––, forthcoming, ‘Intuitionism is allbosh, entirely. Unless it is an inspiration,’ in G. Alberts,L. Bergmans, and F. Muller, (eds.),Significs and the ViennaCircle: Intersections, Dordrecht: Springer.[preprint available online]
• Weyl, H., 1921, ‘Über die neue Grundlagenkrise derMathematik,’Mathematische Zeitschrift, 10:39–70.
• Wittgenstein, L., 1994,Wiener Ausgabe, Band 1, PhilosophischeBemerkungen, Vienna, New York: Springer Verlag.
• Wright, C., 1982, ‘Strict Finitism’,Synthese51(2): 203–282.
• Yessenin-Volpin, A.S., 1970, ‘The ultra–intuitionisticcriticism and the antitraditional program for foundations ofmathematics’, in A. Kino, J. Myhill, and R. Vesley (eds.),Intuitionism and Proof Theory, Amsterdam: North-HollandPublishing Company, 3–45.

Academic Tools

	How to cite this entry.
	Preview the PDF version of this entry at theFriends of the SEP Society.
	Look up topics and thinkers related to this entry at the Internet Philosophy Ontology Project (InPhO).
	Enhanced bibliography for this entryatPhilPapers, with links to its database.

Other Internet Resources

[Please contact the author with suggestions.]

Related Entries

Brouwer, Luitzen Egbertus Jan |category theory |choice, axiom of |Gödel, Kurt | Hilbert, David |Hilbert, David: program in the foundations of mathematics |logic, history of: intuitionistic logic |logic: classical |logic: intuitionistic |mathematics, philosophy of: formalism |mathematics: constructive |phenomenology |Platonism: in metaphysics |set theory |type theory

Acknowledgments

I thank Sebastiaan Terwijn, Mark van Atten, and an anonymous refereefor their useful comments on an earlier draft of this entry.