Constructive mathematics is distinguished from its traditionalcounterpart, classical mathematics, by the strict interpretation ofthe phrase “there exists” as “we canconstruct”. In order to work constructively, we need tore-interpret not only the existential quantifier but all the logicalconnectives and quantifiers as instructions on how to construct aproof of the statement involving these logical expressions.

In this article we introduce modern constructive mathematics based onthe BHK-interpretation of the logical connectives and quantifiers. Wediscuss four major varieties of constructive mathematics, withparticular emphasis on the two varieties associated with Errett Bishopand Per Martin-Löf, which can be regarded as minimal constructivesystems. We then outline progress in (informal) constructive reversemathematics, a research programme seeking to identify principles, suchas Brouwer’s fan theorem, that, added to the minimalconstructive varieties, facilitate proofs of important analytictheorems. After a brief discussion of constructive algebra, economics,and finance, the entry ends with two appendices: one on certainlogical principles that hold in classical, intuitionistic, andrecursive mathematics and which, added to Bishop’s constructivemathematics, facilitate the proof of certain useful theorems ofanalysis; and one discussing approaches to a constructive developmentof general topology.

• 1. Introduction
• 2. The Constructive Interpretation of Logic
• 3. Varieties of Constructive Mathematics
  • 3.1 Intuitionistic Mathematics
  • 3.2 Recursive Constructive Mathematics
  • 3.3 Bishop’s Constructive Mathematics
  • 3.4 Martin-Löf’s Constructive Type Theory
• 4. The Axiom of Choice
• 5. Constructive Reverse Mathematics
  • 5.1 Fan theorems in CRM
• 6. Constructive Topology
• 7. Constructive Mathematical Economics and Finance
• 8. Concluding Remarks
• Bibliography
  • References
  • Related Literature
• Academic Tools
• Other Internet Resources
• Related Entries

1. Introduction

Before mathematicians assert something (other than an axiom) they aresupposed to have proved it true. What, then, do mathematicians meanwhen they assert a disjunction \(P \vee Q\), where \(P\) and \(Q\) aresyntactically correct statements in some (formal or informal)mathematical language? A natural — although, as we shall see,not the unique — interpretation of this disjunction is that notonly does (at least) one of the statements \(P, Q\) hold, but also wecan decide which one holds. Thus just as mathematicians will assert\(P\) only when they have decided that \(P\) holds by proving it, theymay assert \(P \vee Q\) only when they either can produce a proof of\(P\) or else produce one of \(Q\).

With this interpretation, however, we run into a serious problem inthe special case where \(Q\) is the negation, \(\neg P\), of \(P\). Toassert \(\neg P\) is to show that \(P\) implies a contradiction (suchas \(0 = 1)\). But it will often be that mathematicians have neither aproof of \(P\) nor one of \(\neg P\). To see this, we need onlyreflect on the followingGoldbach conjecture (GC):

Every even integer \(\gt 2\) can be written as a sum of twoprimes,

which remains neither proved nor disproved despite the best efforts ofmany of the leading mathematicians since it was first raised in aletter from Goldbach to Euler in 1742. We are forced to conclude that,under the very natural decidability interpretation of P\(\vee Q\), only a stubborn optimist can retain a belief in thelaw of excluded middle (LEM):

For every statement \(P\), either \(P\) or \(\neg P\) holds.

Classical logic gets round this by widening the interpretation of disjunction: itinterprets \(P \vee Q\) as \(\neg(\neg P\wedge \neg Q)\), or in otherwords, “it is contradictory that both \(P\) and \(Q\) befalse”. In turn, this leads to theidealisticinterpretation of existence, in which \(\exists xP(x)\) means \(\neg\forall x\neg P(x)\) (“it is contradictory that \(P(x)\) befalse for every \(x\)”). It is on these interpretations ofdisjunction and existence that mathematicians have built the grand,and apparently impregnable, edifice of classical mathematics whichserves a foundation for the physical, the social, and (increasingly)the biological sciences. However, the wider interpretations come at acost: for example, when we pass from our initial, naturalinterpretation of \(P \vee Q\) to the unrestricted use of theidealistic one, \(\neg(\neg P\wedge \neg Q)\), the resultingmathematics cannot generally be interpreted within computationalmodels such as recursive function theory.

This point is illustrated by a well-worn example, the proposition:

There exist irrational numbers \(a, b\) such that \(a^b\) isrational.

A slick classical proof goes as follows. Either\(\sqrt{2}^{\sqrt{2}}\) is rational, in which case we take \(a = b =\sqrt{2}\); or else \(\sqrt{2}^{\sqrt{2}}\) is irrational, in whichcase we take \(a = \sqrt{2}^{\sqrt{2}}\) and \(b = \sqrt{2}\) (seeDummett 1977 [2000], 6). But as it stands, this proof does not enableus to pinpoint which of the two choices of the pair \((a,b)\) has therequired property. In order to determine the correct choice of\((a,b)\), we would need to decide whether \(\sqrt{2}^{\sqrt{2}}\) isrational or irrational, which is precisely to employ our initialinterpretation of disjunction with \(P\) the statement“\(\sqrt{2}^{\sqrt{2}}\) is rational”.

Here is another illustration of the difference betweeninterpretations. Consider the following simple statement about the set\(\bR\) of real numbers:

where, for reasons that we divulge shortly, \(x \ne 0\) means that wecan find a rational number \(r\) with \(0 \lt r \lt \abs{x}\). Anatural computational interpretation of (*) is that we have aprocedure which, applied to any real number \(x\), either tells usthat \(x = 0\) or else tells us that \(x \ne 0\). (For example, such aprocedure might output 0 if \(x = 0\), and 1 if \(x \ne 0\).) However,because the computer can handle real numbers only by means of finiterational approximations, we have the problem ofunderflow, inwhich a sufficiently small positive number can be misread as 0 by thecomputer; so there cannot be a decision procedure that justifies thestatement (*). In other words, we cannot expect (*) to hold under ournatural computational interpretation of the quantifier \(\forall\) andthe connective \(\vee\).

Let’s examine this from another angle. Let \(G(n)\) act asshorthand for the statement “\(2n + 2\) is a sum of twoprimes”, where \(n\) ranges over the positive integers, anddefine an infinite binary sequence \(\ba = (a_1 ,a_2,\ldots)\) asfollows:

There is no question that \(\ba\) is a computationally well-definedsequence, in the sense that we have an algorithm for computing \(a_n\)for each \(n\): check the even numbers \(4,6,8,\ldots ,2n+2\) todetermine whether each of them is a sum of two primes; in that case,set \(a_n = 0\), and in the contrary case, set \(a_n = 1\). Nowconsider the real number whose \(n\)^th binary digit is\(a_n\):

If (*) holds under our computational interpretation, then we candecide between the following two alternatives:

• \(2^{-1}a_1 + 2^{-2}a_2 + \cdots = 0\), which implies that \(a_n =0\) for every \(n\);
• we can find a positive integer \(N\) such that \(2^{-1}a_1 +2^{-2}a_2 + \cdots \gt 2^{-N}\).

In the latter case, by testing \(a_1 ,\ldots ,a_N\), we can find \(n\le N\) such that \(a_n = 1\). Thus the computational interpretationof (*) enables us to decide whether there exists \(n\) such that \(a_n= 1\); in other words, it enables us to decide the status of theGoldbach Conjecture. An example of this type, showing that aconstructive proof of some classical result \(P\) would enable us tosolve the Goldbach conjecture (and, by similar arguments, many otherhitherto open problems, such as the Riemann hypothesis), is called aBrouwerian example for, or even aBrouweriancounterexample to, the statement \(P\) (though it is not acounterexample in the normal sense of that word).

The use of the Goldbach Conjecture here is purely dramatic. For, theargument of the preceding paragraph can be modified to show that,under our computational interpretation, (*) implies thelimitedprinciple of omniscience (LPO):

For each binary sequence \((a_1 ,a_2, \ldots)\) either \(a_n = 0\) forall \(n\) or else there exists \(n\) such that \(a_n = 1\),

which is generally regarded as an essentially nonconstructiveprinciple for several reasons. First, its recursiveinterpretation,

There is a recursive algorithm which, applied to any recursivelydefined binary sequence \((a_1 ,a_2, \ldots)\), outputs 0 if \(a_n =0\) for all \(n\), and outputs 1 if \(a_n = 1\) for some \(n\),

is provably false within recursive function theory, even withclassical logic (see Bridges & Richman [1987], Chapter 3); so ifwe want to allow a recursive interpretation of all our mathematics,then we cannot use LPO. Secondly, there is a model theory (Kripkemodels) in which it can be shown that LPO is not constructivelyderivable (Bridges & Richman [1987], Chapter 7).

2. The Constructive Interpretation of Logic

It should, by now, be clear that a full-blooded computationaldevelopment of mathematics disallows the idealistic interpretations ofdisjunction and existence upon which most classical mathematicsdepends. In order to work constructively, we need to return from theclassical interpretations to the natural constructive ones:

TheseBHK-interpretations (the name reflects their origin inthe work of Brouwer, Heyting, and Kolmogorov) can be made more preciseusing Kleene’s notion ofrealizability; see (Dummett[1977/2000], 222–234; Beeson [1985], Chapter VII).

There is a common misunderstanding that constructive mathematics isjust mathematics without proofs by contradiction (reductio-ad-absurdumarguments). This isnot the case. Consider typical proofsthat \(\sqrt{2}\) is irrational: these start with the assumption'\(\sqrt{2}\) is rational', then proceed by elementary, and fullyconstructive, steps to arrive at a contradiction. Such a procedure isa perfectly constructive proof that \(\sqrt{2}\) is not rational;indeed, the constructive interpretation of '\(\neg p\)' is preciselythat assuming \(p\) leads to a contradiction. The misunderstandingalluded to at this start of this paragraph is caused by confusing aproof, like the foregoing, of a negated statement with one of thefollowing type: assume \(\neg p\), derive a contradiction, andconclude that \(p\) must hold. From a constructive point of view, themost one can obtain from the latter type of proof is the conclusion\(\neg\neg p\); the final step, claiming that \(p\) must hold, isnonconstructive.

To reinforce this point, consider a proof of the form

Assume there is no such thing as a boojum; then argue constructivelyto arrive at a contradiction.

Such a proof does not normally contain the algorithmic informationenabling us to establishconstructively that there exists aboojum after all. More formally, a constructive proof of \(\neg\neg\exists x P(x)\) does not automatically allow us to conclude that\(\exists x P(x)\).

To summarise: to prove \(\neg p\), we may, and normally do, assume\(p\) and derive a contradiction. To prove \(p\), it isnotenough to assume \(\neg p\) and derive a contradiction.

We turn now to intuitionistic logic in practice. What sort of thingsare we looking for if we are serious about developing mathematics insuch a way that when a theorem asserts the existence of an object\(x\) with a property \(P(x)\), then the proof of the theorem embodiesalgorithms for constructing \(x\) and for demonstrating, by whatevercalculations are necessary, that \(x\) has the property \(P(x)\). Hereare some examples of theorems, each followed by an informaldescription of the requirements for its constructive proof.

1. For each real number \(x\), either \(x = 0\) or \(x \ne 0\).

   Proof requirement: An algorithm which, applied to a givenreal number \(x\), decides whether \(x = 0\) or \(x \ne 0\). Notethat, in order to make this decision, the algorithm might use not onlythe data describing \(x\) but also the data showing that \(x\) isactually a real number.

2. Each nonempty subset \(S\) of \(\bR\)that is bounded abovehas a least upper bound.

   Proof requirement: An algorithm which, applied to a set \(S\)of real numbers, a member \(s\) of \(S\), and an upper bound for\(S\),

   1. computes an object \(b\) and shows that \(b\) is a realnumber;
   2. shows that \(x \le b\) for each \(x \in S\); and
   3. given a real number \(b' \lt b\), computes an element \(x\) of\(S\) such that \(x \gt b'\).
3. If \(f\) is a continuous real-valued mapping on the closedinterval \([0,1]\) such that \(f(0)\cdot f(1) \lt 0\), then thereexists \(x\) such that \(0 \lt x \lt 1\) and \(f(x) = 0\).

   Proof requirement: An algorithm which, applied to thefunction \(f\), a modulus of continuity for \(f\), and the values\(f(0)\) and \(f(1)\),

   1. computes an object \(x\) and shows that \(x\) is a real numberbetween 0 and 1; and
   2. shows that \(f(x) = 0\).
4. If \(f\) is a continuous real-valued mapping on the closedinterval \([0,1]\) such that \(f(0)\cdot f(1) \lt 0\), then for each\(\varepsilon \gt 0\) there exists \(x\) such that \(0 \lt x \lt 1\)and \(\abs{f(x)} \lt \varepsilon\).

   Proof requirement: An algorithm which, applied to thefunction \(f\), a modulus of continuity for \(f\), the values \(f(0)\)and \(f(1)\), and a positive number \(\varepsilon\),

   1. computes an object \(x\) and shows that \(x\) is a real numberbetween 0 and 1; and
   2. shows that \(\abs{f(x)} \lt \varepsilon\).

We already have reasons for doubting that (A) has a constructiveproof. If the proof requirements for (B) can be fulfilled, then, givenany mathematical statement \(P\), we can apply our proof of (B) tocompute a rational approximation \(z\) to the supremum \(\sigma\) ofthe set

with error \(\lt \bfrac{1}{4}\). We can then determine whether \(z \gt\bfrac{1}{4}\), in which case \(\sigma \gt 0\), or \(z \lt\bfrac{3}{4}\), when \(\sigma \lt 1\). In the first case, there exists\(x \in S\) with \(x \gt 0\), so we must have \(x = 1\) and therefore\(P\). In the case \(\sigma \lt 1\), we have \(\neg P\). Thus (B)implies the law of excluded middle.

However, in Bishop’s constructive theory of the real numbers,based on Cauchy sequences with a preassigned convergence rate, we canprove the followingconstructive least-upper-boundprinciple:

Let \(S\) be a nonempty subset of \(\bR\) that is bounded above. Then\(S\) has a least upper bound if and only if it isupper-orderlocated, in the sense that for all real numbers \(\alpha ,\beta\) with \(\alpha \lt \beta\), either \(\beta\) is an upper boundfor \(S\) or else there exists \(x \in S\) with \(x \gt \alpha\)(Bishop & Bridges [1985], p. 37, Proposition (4.3)).

In passing, we mention an alternative development of the constructivetheory of \(\bR\) based on interval arithmetic; see Chapter 2 ofBridges & Vîță [2006].

Each of statements (C) and (D), which are classically equivalent, is aversion of the Intermediate Value Theorem. In these statements, amodulus of continuity for \(f\) is a set \(\Omega\) ofordered pairs \((\varepsilon ,\delta)\) of positive real numbers withthe following two properties:

• for each \(\varepsilon \gt 0\) there exists \(\delta \gt 0\) suchthat \((\varepsilon ,\delta) \in \Omega\)
• for each \((\varepsilon , \delta) \in \Omega\), and for all \(x,y\in [0,1]\) with \(\abs{x - y} \lt \delta\), we have \(\abs{f(x) -f(y)} \lt \varepsilon\).

Statement (C) entails another essentially nonconstructive principle,thelesser limited principle of omniscience(LLPO):

For each binary sequence \((a_1,a_2,\ldots)\) with at most one termequal to 1, either \(a_n = 0\) for all even \(n\) or else \(a_n = 0\)for all odd \(n\).

Statement (D), a weak form of (C), can be proved constructively, usingan interval-halving argument of a standard type. The followingstronger constructive intermediate value theorem, which suffices formost practical purposes, is proved using anapproximate-interval-halving argument:

Let \(f\) be a continuous real-valued mapping on the closed interval\([0,1]\) such that \(f(0)\cdot f(1) \lt 0\). Suppose also that \(f\)islocally nonzero, in the sense that for each \(x \in[0,1]\) and each \(r \gt 0\), there exists \(y\) such that \(\abs{x -y} \lt r\) and \(f(y) \ne 0\). Then there exists \(x\) such that \(0\lt x \lt 1\) and \(f(x) = 0\).

The situation of the intermediate value theorem is typical of many inconstructive analysis, where we find one classical theorem withseveral constructive versions, some or all of which may be equivalentunder classical logic.

There is one omniscience principle whose constructive status is lessclear than that ofLPO andLLPO—namely,Markov’s principle (MP):

For each binary sequence \((a_n)\), if it is contradictory that allthe terms \(a_n\) equal 0, then there exists a term equal to 1.

This principle is equivalent to a number of simple classicalpropositions, including the following:

• For each real number \(x\), if it is contradictory that \(x\)equal 0, then \(x \ne 0\) (in the sense we mentioned earlier).
• For each real number \(x\), if it is contradictory that \(x\)equal 0, then there exists \(y \in \bR\) such that \(xy = 1\).
• For each one-one continuous mapping \(f : [0,1] \rightarrow \bR\),if \(x \ne y\), then \(f(x) \ne f(y)\).

Markov’s principle represents an unbounded search: if you have aproof that all terms \(a_n\) being 0 leads to a contradiction, then,by testing the terms \(a_1,a_2,a_3,\ldots\) in turn, you areguaranteed to come across a term equal to 1; but this guarantee doesnot extend to an assurance that you will find the desired term beforethe end of the universe. Most practitioners of constructivemathematics view Markov’s principle with at least suspicion, ifnot downright disbelief. Such views are reinforced by the observationthat there is a Kripke Model showing thatMP is notconstructively derivable (Bridges & Richman [1987],137–138.)

3. Varieties of Constructive Mathematics

The desire to retain the possibility of a computational interpretationis one motivation for using the constructive reinterpretations of thelogical connectives and quantifiers that we gave above; but it is notexactly the motivation of the pioneers of constructivism inmathematics. In this section we look at some of the differentapproaches to constructivism in mathematics over the past 130years.

3.1 Intuitionistic Mathematics

In the late nineteenth century, certain individuals—most notablyKronecker and Poincaré—had expressed doubts about, oreven disapproval of, the idealistic, nonconstructive methods used bysome of their contemporaries; but it is in the polemical writings ofL.E.J. Brouwer (1881–1966), beginning with his Amsterdam doctoral thesis,Brouwer [1907], and continuing over the next forty-seven years, thatthe foundations of a precise, systematic approach to constructivemathematics were laid. In Brouwer’s philosophy, known asintuitionism, mathematics is a free creation of the human mind, and an objectexists if and only if it can be (mentally) constructed. If one takesthat philosophical stance, then one is inexorably drawn to theforegoing constructive interpretation of the logical connectives andquantifiers: for how could a proof of the impossibility of thenon-existence of a certain object \(x\) describe a mental constructionof \(x\)?

Brouwer was not the clearest expositor of his ideas, as is shown bythe following quotation:

Mathematics arises when the subject of two-ness, which results fromthe passage of time, is abstracted from all special occurrences. Theremaining empty form [the relation of \(n\) to \(n+1\)] of the commoncontent of all these two-nesses becomes the original intuition ofmathematics and repeated unlimitedly creates new mathematicalsubjects. (quoted in Kline [1972], 1199–2000)

A modern version of Brouwer’s view was given by Errett Bishop(Bishop [1967], p. 2):

The primary concern of mathematics is number, and this means thepositive integers. We feel about number the way Kant felt about space.The positive integers and their arithmetic are presupposed by the verynature of our intelligence and, we are tempted to believe, by the verynature of intelligence in general. The development of the positiveintegers from the primitive concept of the unit, the concept ofadjoining a unit, and the process of mathematical induction carriescomplete conviction. In the words of Kronecker, the positive integerswere created by God.

However obscure Brouwer’s writings could be, one thing wasalways clear: for him, mathematics took precedence over logic. Onemight say, as Hermann Weyl did in the following passage, that Brouwersaw classical mathematics as flawed precisely in its use of classicallogic without reference to the underlying mathematics:

According to [Brouwer’s] view and reading of history, classicallogic was abstracted from the mathematics of finite sets and theirsubsets. … Forgetful of this limited origin, one afterwardsmistook that logic for something above and prior to all mathematics,and finally applied it, without justification, to the mathematics ofinfinite sets. This is the Fall and original sin of set theory, forwhich it is justly punished by the antinomies. It is not that suchcontradictions showed up that is surprising, but that they showed upat such a late stage of the game. (Weyl [1946])

In particular, this misuse of logic led to nonconstructive existenceproofs which, in Weyl’s words, “inform the world that atreasure exists without disclosing its location”.

In order to describe the logic used by the intuitionist mathematician,it was necessary first to analyse the mathematical processes of themind, from which analysis the logic could be extracted. In 1930,Brouwer’s most famous pupil, Arend Heyting, published a set offormal axioms which so clearly characterise the logic used by theintuitionist that they have become universally known as the axioms forintuitionistic logic (Heyting [1930]). These axioms captured the informalBHK-interpretation of the connectives and quantifiers that we gaveearlier.

Intuitionistic mathematics,INT, diverges from other types ofconstructive mathematics in its interpretation of the term“sequence”. Normally, a sequence in constructivemathematics is given by a rule which determines, in advance, how toconstruct each of its terms; such a sequence may be said to belawlike orpredeterminate. Brouwer generalised thisnotion of a sequence to include the possibility of constructing theterms one-by-one, the choice of each term being made freely, orsubject only to certain restrictions stipulated in advance. Mostmanipulations of sequences do not require that they be predeterminate,and can be performed on these more generalfree choicesequences.

Thus, for the intuitionist, a real number \(\bx = (x_1,x_2,\ldots)\)—essentially, a Cauchy sequence of rationalnumbers—need not be given by a rule: its terms \(x_1,x_2,\ldots\), are simply rational numbers, successively constructed,subject only to some kind of Cauchy restriction such as the followingone used by Bishop [1967]:

Once free choice sequences are admitted into mathematics, so, perhapsto one’s initial surprise, are certain strong choice principles.Let \(P\) be a subset of \(\bN^{\bN} \times \bN\) (where \(\bN\)denotes the set of natural numbers and, for sets \(A\) and \(B, B^A\)denotes the set of mappings from \(A\) into \(B)\), and suppose thatfor each \(\ba \in \bN^{\bN}\) there exists \(n \in \bN\) such that\((\ba,n) \in P\). From a constructive point of view, this means thatwe have a procedure, applicable to sequences, that computes \(n\) forany given \(\ba\). According to Brouwer, the construction of anelement of \(\bN^{\bN}\) is forever incomplete: a generic sequence\(\ba\) ispurely extensional, in the sense that at any givenmoment we can know nothing about \(\ba\) other than a finite set ofits terms. It follows that our procedure must be able to calculate,from some finite initial sequence \((a_0 ,\ldots ,a_N)\) of terms of\(\ba\), a natural number \(n\) such that \(P(\ba,n)\). If \(\bb \in\bN^{\bN}\) is any sequence such that \(b_{k} = a_{k}\) for \(0 \le k\le N\), then our procedure must return the same \(n\) for \(\bb\) asit does for \(\ba\). This means that \(n\) is a continuous function of\(\ba\) with respect to the topology on \(\bN^{\bN}\) given by themetric

We are therefore led to the followingprinciple of continuouschoice, which we divide into a continuity part and a choice part.

If \(P\) and \(f\) are as in CC2, then we say that \(f\) is achoice function for \(P\).

The omniscience principles LPO and LLPO are demonstrably false underthe hypotheses CC1–2; but MP is consistent with it. Among theremarkable consequences of CC1–2 are the following.

• Any function from \(\bN^{\bN}\) or \(2^{\bN}\) to a metric spaceis pointwise continuous.
• Every mapping from a nonempty complete separable metric space to ametric space is pointwise continuous.
• Every map from the real line \(\bR\) to itself is pointwisecontinuous.
• Let \(X\) be a complete separable normed space, \(Y\) a normedspace, and \((u_n)\) a sequence of linear mappings from \(X\) to \(Y\)such that for each unit vector \(x\) of \(X\), \[\phi(x) = \sup\{ \Vert u_n(x)\rVert : n \in \bN \}\]

  exists. Then there exists \(c \gt 0\) such that \(\lVert u_n (x)\rVert\le c\) for all \(n\in \bN\) and all unit vectors \(x\) of \(X\)(Uniform boundedness principle).

Each of these statements appears to contradict known classicaltheorems. However, the comparison with classical mathematics shouldnot be made superficially: in order to understand that there is noreal contradiction here, we must appreciate that the meaning of suchterms as “function” and even “real number” inintuitionistic mathematics is quite different from that in theclassical setting. (In practice, intuitionistic mathematics cannot becompared, readily and directly, with classical mathematics.)

Brouwer’s introspection over the nature of functions and thecontinuum led him to a second principle, which, unlike that ofcontinuous choice, is classically valid. This principle requires alittle more background for its explanation.

For any set \(S\) we denote by \(S^*\) the set of all finite sequencesof elements of \(S\), including the empty sequence \((\ )\). If\(\alpha = (a_1 ,\ldots ,a_n)\) is in \(S^*\), then \(n\) is calledthelength of \(\alpha\) and is denoted by \(\abs{\alpha}\).If \(m \in \bN\), and \(\alpha\) is a finite or infinite sequence in\(S\) of length at least \(m\), then we denote by \(\bar{\alpha}(m)\)the finite sequence consisting of the first \(m\) terms of \(\alpha\).Note that \(\bar{\alpha}(0) = (\ )\) and \(\abs{\bar{\alpha}(0)}\) = 0. If \(\alpha \in S^*\) and \(\beta = \bar{\alpha}(m)\) for some\(m\), we say that \(\alpha\) is anextension of \(\beta\),and that \(\beta\) is arestriction of \(\alpha\).

A subset \(\sigma\) of \(S\) is said to bedetachable (from\(S)\) if

A detachable subset \(\sigma\) of \(\bN^*\) is called afanif

• it is closed under restriction: for each \(\alpha \in \bN^*\) andeach \(n\), if \(\bar{\alpha}(n) \in S\), then \(\bar{\alpha}(k) \inS\) whenever \(0 \le k \le n\); and
• for each \(\alpha \in \sigma\), the set \[\{ \alpha^* n \in S: n \in \bN \}\]

  is finite or empty, where \(\alpha^* n\) denotes the finite sequenceobtained by adjoining the natural number \(n\) to the terms of\(\alpha\).

Apath in a fan \(\sigma\) is a sequence \(\alpha\), finiteor infinite, such that \(\bar{\alpha}(n) \in \sigma\) for eachapplicable \(n\). We say that a path \(\alpha\) isblocked bya subset \(B\) if some restriction of \(\alpha\) is in \(B\); if norestriction of \(\alpha\) is in \(B\), we say that \(\alpha\)misses \(B\). A subset \(B\) of a fan \(\sigma\) is called abar for \(\sigma\) if each infinite path of \(\sigma\) isblocked by \(B\); a bar \(B\) for \(\sigma\) isuniform ifthere exists \(n \in \bN\) such that each path of length \(n\) isblocked by \(B\).

At last we can state Brouwer’s next principle of intuitionism,the fan theorem for detachable bars (FT\(_D\)):

Every detachable bar of a fan is uniform.

In its classical contrapositive form, FT\(_D\) is known asKönig’s Lemma: if for every \(n\) there exists apath of length \(n\) that misses \(B\), then there exists an infinitepath that misses \(B\) (see Dummett 1977 [2000], 49–53). (Ofcourse, classically the condition of detachability is superfluous.) Itis simple to construct a Brouwerian counterexample toKönig’s Lemma.

Brouwer actually posited the fan theorem without the restriction ofdetachability of the bar. Attempts to prove that more general fantheorem constructively rely on an analysis of how we could know that asubset is a bar, and led Brouwer to a notion ofbarinduction; this is discussed in Section 3.6 of the entry onintuitionism in the philosophy of mathematics; another good reference for bar induction is van Atten (2004). Weshall return to fan theorems in Section 4.

Of the many applications of Brouwer’s principles, the mostfamous is hisuniform continuity theorem (which follows fromthe pointwise continuity consequences of CC1-2 together a form of fantheorem more general than FT\(_D)\):

Every mapping from a compact (that is, complete, totally bounded)metric space into a metric space is uniformly continuous.

The reader is warned once again to interpret this carefully withinBrouwer’s intuitionistic framework, and not to jump to theerroneous conclusion that intuitionism contradicts classicalmathematics. It is more sensible to regard the two types ofmathematics as incomparable. For further discussion, see the entry onintuitionistic logic.

Unfortunately — and perhaps inevitably, in the face ofopposition from mathematicians of such stature as Hilbert —Brouwer’s intuitionist school of mathematics and philosophybecame more and more involved in what, at least to classicalmathematicians, appeared to be quasi-mystical speculation about thenature of constructive thought, to the detriment of the practice ofconstructive mathematics itself. This unfortunate polarisation betweenthe Brouwerians and the Hilbertians culminated in the notoriousGrundlagenstreit of the 1920s, details of which can be found in theBrouwer biographies by van Dalen [1999, 2005] and van Stigt[1990].

3.2 Recursive Constructive Mathematics

In the late 1940s, the Russian mathematician A.A. Markov began thedevelopment of an alternative form of constructive mathematics,RUSS, which is, essentially,recursive function theory with intuitionistic logic (Markov [1954], Kushner [1985]). Inthis variety the objects are defined by means ofGödel-numberings, and the procedures are all recursive; the maindistinction between RUSS and the classical recursive analysisdeveloped after the work of Turing, Church, and others in 1936clarified the nature of computable processes is that the logic used inRUSS is intuitionistic.

One obstacle faced by the mathematician attempting to come to gripswith RUSS is that, being expressed in the language of recursiontheory, it is not easily readable; indeed, on opening a page ofKushner’s excellent lectures [1985], one might be forgiven forwondering whether this is analysis or logic. (This remark should betempered with reference to the two relatively readable books onclassical recursive analysis by Aberth [1980, 2001].) Fortunately, onecan get to the heart of RUSS by an axiomatic approach due to Richman[1983] (see also Chapter 3 of Bridges & Richman [1987]).

First, we define a set \(S\) to becountable if there is amapping from a detachable subset of \(\bN\) onto \(S\). Withintuitionistic logic we cannot prove that every subset of \(\bN\) isdetachable (the reader is invited to provide a Brouwerian example todemonstrate this). Countable subsets of \(\bN\) in Richman’saxiomatic approach are the counterparts of recursively enumerable setsin the normal development of RUSS.

By apartial function on \(\bN\) we mean a mapping whosedomain is a subset of \(\bN\); if the domain is \(\bN\) itself, thenwe call the function atotal function on \(\bN\).Richman’s approach to RUSS is based on intuitionistic logic anda single axiom ofcomputable partial functions(CPF):

There is an enumeration \(\phi_0 ,\phi_1,\ldots\) of the set of allpartial functions from \(\bN\) to \(\bN\) with countable domains.

It is remarkable what can be deduced cleanly and quickly using thisprinciple. For example, we can prove the following result, whichalmost immediately shows thatLLPO, and henceLPO, arefalse in the recursive setting.

There is a total function \(f : \bN \times \bN \rightarrow \{0,1\}\)such that

• for each \(m\) there exists at most one \(n\) such that \(f(m,n) =1\); and
• for each total function \(f : \bN \rightarrow \{0,1\}\), thereexist \(m,k\) in \(\bN\) such that \(f(m,2k+f(m)) = 1\).

Of more interest, however, are results such as the following withinRUSS.

• Specker’s Theorem (Specker [1949]): There exists astrictly increasing sequence \((r_1 ,r_2,\ldots)\) of rational numbersin the closed interval \([0,1]\) such that for each \(x \in \bR\)there exist \(N \in \bN\) and \(\delta \gt 0\) such that \(\abs{x -r_n} \ge \delta\) for all \(n \ge N\).
• For each \(\varepsilon \gt 0\), there exists a sequence \((I_1,I_2,\ldots)\), of bounded open intervals in \(\bR\) such that \(\bR\subseteq \bigcup_{n=1}^{\infty} I_n\) and \(\sum_{n=1}^N \abs{I_n}\lt \varepsilon\) for each N. (Such a sequence of intervals is calledan \(\varepsilon\)-singular cover of \(\bR\).)
• There exists a pointwise continuous function \(f : [0,1]\rightarrow \bR\) that is not uniformly continuous.
• There exists a positive-valued uniformly continuous function \(f :[0,1] \rightarrow \bR\) whose infimum is 0.

From a classical viewpoint, these results fit into place when onerealises that words such as “function” and “realnumber” should be interpreted as “recursivefunction” and “recursive real number” respectively.Note that the second of the above four recursive theorems is a strongrecursive counterexample to the open-cover compactness property of the(recursive) real line; and the fourth is a recursive counterexample tothe classical theorem that every uniformly continuous mapping of acompact set into \(\bR\) attains its infimum.

3.3 Bishop’s Constructive Mathematics

Progress in all varieties of constructive mathematics was relativelyslow throughout the next decade and a half. What was needed to raisethe profile of constructivism in mathematics was a top-rankingclassical mathematician to show that a thoroughgoing constructivedevelopment of deep analysis was possible without a commitment toBrouwer’s non-classical principles or to the machinery ofrecursive function theory. This need was fulfilled in 1967, with theappearance of Errett Bishop’s monographFoundations ofConstructive Analysis [1967] (see also Bishop & Bridges[1985]), the product of an astonishing couple of years in which,working in the informal but rigorous style used by normal analysts,Bishop provided a constructive development of a large part oftwentieth-century analysis, including the Stone-Weierstrass Theorem,the Hahn-Banach and separation theorems, the spectral theorem forself-adjoint operators on a Hilbert space, the Lebesgue convergencetheorems for abstract integrals, Haar measure and the abstract Fouriertransform, ergodic theorems, and the elements of Banach algebratheory. Thus, at a stroke, he gave the lie to the commonly-held viewexpressed so forcefully by Hilbert:

Taking the principle of excluded middle from the mathematician wouldbe the same, say, as proscribing the telescope to the astronomer or tothe boxer the use of his fists. (Hilbert [1928])

Not only did Bishop’s mathematics,BISH, have theadvantage of readability — if you open Bishop’s book atany page, what you see is clearly recognisable as analysis, even if,from time to time, his moves in the course of a proof may appearstrange to one schooled in the use of the law of excluded middle— but, unlike intuitionistic or recursive mathematics, it admitsmany different interpretations. Intuitionistic mathematics, recursiveconstructive mathematics, and even classical mathematics all providemodels of BISH. In fact, the results and proofs in BISH can beinterpreted, with at most minor amendments, in any reasonable model ofcomputable mathematics, such as, for example, Weihrauch’s TypeTwo Effectivity Theory (Weihrauch [2000]; Bauer [2005]).

How is this multiple interpretability achieved? At least in part byBishop’s refusal to pin down his primitive notion of“algorithm” or, in his words, “finiteroutine”. This refusal has led to the criticism that hisapproach lacks the precision that a logician would normally expect ofa foundational system. However, this criticism can be overcome bylooking more closely at what practitioners of BISH actually do whenthey prove theorems: in practice, they are doingmathematics withintuitionistic logic. Experience shows that the restriction tointuitionistic logic always forces mathematicians to work in a mannerthat, at least informally, can be described as algorithmic; soalgorithmic mathematics appears to be equivalent to mathematicsthat uses only intuitionistic logic. If that is the case, then wecan practice constructive mathematics using intuitionistic logic onany reasonably defined mathematical objects, not just some class of“constructive objects”.

This view, more or less, appears to have first been put forward byRichman [1990, 1996]. Taking the logic as the primary characteristicof constructive mathematics, it does not reflect the primacy ofmathematics over logic that was part of the belief of Brouwer,Heyting, Markov, Bishop, and other pioneers of constructivism. On theother hand, it does capture the essence of constructive mathematics inpractice.

Thus one might distinguish between theontologicalconstructivism of Brouwer and others who are led to constructivemathematics through a belief that mathematical objects are mentalcreations, and theepistemological constructivism of Richmanand those who see constructive mathematics as characterised by itsmethodology, based on the use of intuitionistic logic. Of course, theformer approach to constructivism inevitably leads to the latter; andthe latter is certainly not inconsistent with a Brouwerianontology.

To do actual mathematics we need more than just intutionistic logic.For Bishop, the building blocks of mathematics were the positiveintegers (see the quote from Bishop [1967] in Section 3.1 above).Among the early formal systems for BISH were Myhill’s[1975] axiomatic foundation based on primitive notions of number, set,and function; Feferman’s [1975] system forexplicitmathematics; and Friedman’s [1977] intuitionistic ZF settheory. The two most favoured formal underpinnings of BISH atthis stage areconstructive Zermelo-Fraenkel set theory (CZF), in Aczel and Rathjen [2010, in Other Internet Resources], andintuitionistic type theory, in Martin-Löf [1975, 1984].

3.4 Martin-Löf’s Constructive Type Theory

Before ending our tour of varieties of modern constructivemathematics, we visit a fourth variety,ML, based on PerMartin-Löf’sintuitionistic type theory. Martin-Löf published hisNotes on ConstructiveMathematics [1968], based on lectures he had given in Europe in1966–68; so his involvement with constructivism in mathematicsgoes back at least to the period of Bishop’s writing ofFoundations of Constructive Analysis. Martin-Löf’sbook is in the spirit of RUSS, rather than BISH; indeed, its authordid not have access to Bishop’s book until his own manuscriptwas finished. Martin-Löf later turned his attention to his theoryof types as a foundation for Bishop-style constructive mathematics.

Here, in his own words, is an informal explanation of the ideasunderlying ML:

We shall think ofmathematical objects orconstructions. Every mathematical object is of a certain kindortype [… and] is always given together with itstype. … A type is defined by describing what we have to do inorder to construct an object of that type. … Put differently, atype is well-defined if we understand … what it means to be anobject of that type. Thus, for instance \(\bN \rightarrow \bN\)[functions from \(\bN\) to \(\bN\)] is a type, not because we knowparticular number theoretic functions like the primitive recursiveones, but because we think we understand the notion of numbertheoretic functionin general. (Martin-Löf [975])

In particular, in this system every proposition can be represented asa type: namely, the type of proofs of the proposition. Conversely,each type determines a proposition: namely, the proposition that thetype in question is inhabited. So when we think of a certain type\(T\) as a proposition, we interpret the formula

as “\(x\) is a proof of the proposition \(T\)”.

Martin-Löf goes on to construct new types, such as Cartesianproducts and disjoint unions, from old. For example, the Cartesianproduct

is the type of functions that take an arbitrary object \(x\) of type\(A\) into an object of type \(B(x)\). In the propositions-as-proofsinterpretation, where \(B(x)\) represents a proposition, the aboveCartesian product corresponds to the universal proposition

Martin-Löf distinguishes carefully between proofs andderivations: aproof object is a witness to the fact thatsome proposition has been proved; whereas aderivation is therecord of the construction of a proof object. Also, he exercises twobasic forms (one dare not say “types” here) ofjudgement. The first is a relation between proof objects andpropositions, the second a property of some propositions. In the firstcase, the judgement is either one that a proof object \(a\) is awitness to a proposition \(A\), or else one that two proof objects\(a\) and \(b\) are equal and both witness that \(A\) has been proved.The first case of the second form of judgement states that aproposition \(A\) is well-formed, and the second records that twopropositions \(A\) and \(B\) are equal.

There is a careful, and highly detailed, set of rules for formalisingML. We will not go into those here, but refer the reader to othersources such as Sambin & Smith [1998].

When actually doing constructive mathematics in type theory, one oftenneeds to equip completely presented sets (types) with an equivalencerelation, the combination being known as asetoid. Mappingsare then functions that respect those equivalence relations. This isin close agreement with the way Bishop presented his informal theoryof sets. The dependent types of Martin-Löf are useful forconstructing subsets. For instance, the real numbers can beconstructed using the \(\Sigma\)-type (see Martin-Löf[1984]):

An element of this type \(B\) is thereby a pair consisting of aconvergent sequence \(\bx\) of rationals and a proof \(p\) that it isconvergent. A suitable equivalence relation \({\sim}\) on \(R\) isdefined by taking \((x,p)\sim(y,q)\) to mean

The resultingsetoid of real numbers is \(\bR = (R,{\sim})\).We can readily prove that

and then, using the type-theoretic axiom of choice (see Section 4below), find a function \(f : \bR\rightarrow \bZ\) such that \(f(x)\lt x \lt f(x)+2\). However, there is no reason to believe that thefunction \(f\) respects the equivalence relations—that is, that\(f(x) = f(y)\) holds if \(x \sim y\).

Every constructive proof embodies an algorithm that, in principle, canbe extracted and recast as a computer program; moreover, theconstructive proof is itself a verification that the algorithm iscorrect — that is, meets its specification. One major advantageof Martin-Löf’s formal approach to constructive mathematicsis that it greatly facilitates the extraction of programs from proofs.This has led to serious work on the implementation of constructivemathematics in various locations (see Martin-Löf [1980],Constable [1986], Hayashi & Nakano [1988], Schwichtenberg [2009]).Some recent implementations of type theory for proof extraction areCoq and Agda (see the links in Other Internet Resources).

4. Axioms of Choice and the Continuum Hypothesis

The full axiom of choice can be stated as follows:

Now, if this is to hold under a constructive interpretation, then fora given \(x \in A\), the value \(f(x)\) of the choice function willdepend not only on \(x\)but also on the data proving that \(x\)belongs to \(A.\) In general, we cannot expect to produce achoice function of this sort. However, the BHK interpretation of thehypotheses in the axiom is that there is an algorithm \(\mathcal{A}\)which, applied to any given \(x \in A\), produces an element \(y \inB\) such that \((x,y) \in S\). If \(A\) is acompletely presentedset, one for which no work beyond the construction of eachelement in the set is required to prove that the element does indeedbelong to \(A\), then we might reasonably expect the algorithm\(\mathcal{A}\) to be a choice function. In Martin-Löf’stype theory,every set is completely presented and, inkeeping with the BHK interpretation, the axiom of choice isderivable.

On the other hand, in Bishop-style mathematics, completelypresented–––or, in his terminology,basic–––sets are rare, one example being\(\bN\); so we might expect that the axiom of choice would not bederivable. In fact, as was shown by Diaconescu [1975] and Goodman& Myhill [1978], and prefigured by Bishop himself in Problem 2 onpage 58 of Bishop 1967, the axiom of choice implies the law ofexcluded middle. Clearly, the Diaconescu-Goodman-Myhill theoremapplies only under the assumption that not every set is completelypresented.

Constructive mathematicians not working in ML typically reject thefull axiom of choice but embrace the axiom of countable choice, inwhich the domain of choice is \(\bN\), and dependent choice. But someprefer to work without even countable choice, on the grounds that tospeak of an infinity of choices without giving a rule presents adifficulty that is just as great whether or not the infinity isdenumerable. Interestingly, Lebesgue made precisely this point in aletter to Borel (see Moore [2013], page 316):

I agree completely with Hadamard when he states that to speak of aninfinity of choices without giving a rule presents a difficulty thatis just as great whether or not the infinity is denumerable.

The effect of abandoning even countable choice is the exclusion ofmany theorems that, as they stand, are proved using sequential,choice-based arguments. But those who advocate avoiding choice wouldargue that avoiding choice forces you to formulate things better.

A particular case of interest is the Fundamental Theorem of Algebra:every complex polynomial has at least one root in the complex plane.Richman [2000] has shown that without countable choice, although wecan construct only isolated (possibly multiple) roots, we canconstruct arbitrarily close approximations to the multiset of roots.Such an approach focusses on finding an approximate linearfactorization of the polynomial, rather than on finding separateapproximations to each of its roots.

For further analysis of the axiom of choice in set theory and typetheory see Martin-Löf [2006], and the SEP entries oncategory theory,type theory, andintuitionistic type theory.

We now recall thepower set axiom of classical set theory: if\(X\) is a set, then so is itspower set \[\textrm{sb}(X)≡ \{S: S \subset X\}.\] Sincethis definition is impredicative, most constructive mathematicianshesitate to regard \(\textrm{sb}(X)\) as a set. What they normallyuse, and we shall adopt, as the constructive replacement for the powerset axiom is theaxiom of exponentiation: If \(A\) and \(B\)are sets, then so is the set of all mappings from \(A\) into \(B\). Inparticular, the class \(2^{\bN}\) of all binary sequences is a set.

In order to discuss the Continuum Hypothesis, we need notions ofcomparative size for classes \(A\) and \(B\). We say that

• \(A\) isequinumerous with \(B\) if there exists abijective mapping of \(A\) onto \(B\), and that
• \(A\) iscardinally included in \(B\) if \(A\) isequinumerous with a subclass of \(B\).

A consequence of the axiom of replacement in constructiveZermelo–Fraenkel set theory,CZF, is that if \(A\) is a set and \(B\) is a class that is equinumerouswith \(A\), then \(B\) is also a set. It follows that the class\[\textrm{dch}(\bN)≡ \{S \subset\bN : \forall x \in \bN (x \in S \vee x \not\in S)\}\] of detachable subsets of \(\bN\), being equivalent to\(2^{\bN}\), is a set.

Classically, every subset of \(\bN\) is detachable from \(\bN\), so\(\textrm{dch}(\bN)\) = \(\textrm{sb}(\bN)\). But this is not the caseconstructively: if for each statement \(p\) the set \[\{x \in 1 : p \vee \neg p \}\] werein \(\textrm{dch}(\bN)\), then we could derive the law of excludedmiddle.

Theclassical Continuum Hypothesis states that there is noset whose cardinality lies strictly between that of the set \(\bN\)and that of \(\textrm{sb}(\bN)\). We can state this more formally asfollows: \[\forall C(\bN ≲ C≲ \textrm{sb}(\bN) \Rightarrow C \cong \bN \vee C \cong \textrm{sb}(\bN))\] or, equivalently, \[\forall C(\bN ≲ C≲ \textrm{sb}(\bN) \wedge \neg(C ≲ \bN) \Rightarrow C \cong \textrm{sb}(\bN))\] Constructivelyacceptable classical equivalents of these two statements are:\[\forall C(\bN ≲ C ≲ \textrm{dch}(\bN) \Rightarrow C \cong \bN \vee C \cong \textrm{dch}(\bN))\] and the one that we take as ourconstructiveContinuum Hypothesis, \(\textrm{CH}\), \[\forall C(\bN ≲ C≲ \textrm{dch}(\bN) \wedge \neg(C \cong \bN) \Rightarrow C \cong \textrm{dch}(\bN))\]

We sketch a proof that \(\textrm{CH}\) implies the law of excludedmiddle. First we note that \(2^{\bN}\) is uncountable in the strongsense: Cantor’s diagonal argument shows that if \(S\) is a countablesubset of \(2^{\bN}\), then there exists \(f \in 2^{\bN}\) such that\(f \notin S\). Assuming \(\textrm{CH}\), we now define \[X≡ \{S \in \textrm{dch}(\bN) : p \vee \neg p \}\]and \[\textrm{C}≡\bN \cup X.\] Then \(\bN ≲C≲\textrm{dch}(\bN)\). If \(C\cong \bN \), then \(p \vee \neg p \) is false, which is absurd. Hence\(\neg (C \cong \bN)\) and therefore \(C \cong \textrm{dch}(\bN)\).But \(\textrm{dch}(\bN)\), being equinumerous with \(2^{\bN}\) , isuncountable, so there exists \(S \in \textrm{dch}(\bN)\) that does notbelong to the countable subset \(\bN\) of \(\textrm{dch}(\bN)\). Thus\(S \in C \), and therefore \(p \vee \neg p \) holds.

Incidentally, although, in light of the BHK interpretation of'\(\vee\)', the first of our two constructive statements classicallyequivalent to the classical Continuum Hypothesis might appear to bestronger than \(\textrm{CH}\), since the latter implies the law ofexcluded middle it is constructively equivalent to the former.

The foregoing work on \(\textrm{CH}\) can be formalised inCZF, which is equiconsistent with classical Zermelo–Fraenkel settheory,ZF. If we allow ourselves to invoke the Gödel–Cohen theoremthat the Continuum Hypothesis is independent of ZF, then we can drawsome interesting conclusions by looking more closely at our proof that\(\textrm{CH}\) implies LEM. To do so, take \(p=\textrm{CH}\) in ourproof, so that \[X≡ \{S \in \textrm{dch}(\bN) : \textrm {CH} \vee \neg \textrm{CH} \}.\] If \(X=0\), then \(\neg (\textrm{CH} \vee\neg \textrm{CH})\), which is absurd; so \(\neg(X=0)\). On the otherhand, if \(X\) is inhabited — that is, contains a point —then \(\textrm{CH} \vee \neg \textrm{CH}\), so under the constructiveinterpretation of '\(\vee\)', either we have a proof of\(\textrm{CH}\) or else we have a proof of \(\neg \textrm{CH}\). Sincethis runs counter to the aforementioned Gödel–Cohentheorem, we may regard \(X\) as an explicit example of a set that isnot empty but for which it is impossible to construct a member. This,in itself, is not uninteresting; but it also gives a new insight intothe constructive status of \(\textrm{CH}\). From our proof that\(\textrm{CH}\) implies LEM we see that the set \(C≡\bN \cup X\)satisfies \[ \bN≲C≲\textrm{dch}(\bN) \wedge \neg(C \cong \bN). \] Also, \[ \neg(C \cong \textrm{dch}(\bN)) \Rightarrow X=0, \] which is absurd, so\(\neg\neg(C \cong \textrm{dch}(\bN))\). On the other hand,\[C \cong \textrm{dch}(\bN) \Rightarrow \textrm{CH} \vee \neg \textrm{CH}.\] Thus, provided \(\textrm{CH}\) is independent of CZF(which, in view of equiconsistency of CZF and ZF, it had better be),we see that \(C\) is an explicit example of a set that has theproperty \[ \bN≲C≲\textrm{dch}(\bN) \wedge \neg(C\cong \bN) \wedge \neg \neg (C \cong \textrm{dch}(\bN)) \] but, within CZF, cannot be proved equinumerouswith \(\textrm{dch}(\bN)\).

5. Constructive Reverse Mathematics

In the 1970s, Harvey Friedman initiated a research programme ofreverse mathematics, aiming to classify mathematical theoremsaccording to their equivalence to one of a small number ofset-theoretic principles (Friedman 1975). This classification revealsinteresting, sometimes remarkable, differences in proof-theoreticcomplexity. For example, although the Ascoli–Arzelàtheorem is used in the standard proof of Peano’s existencetheorem for solutions of ordinary differential equations (Hurewicz[1958], page 10), a reverse-mathematical analysis shows that theformer is equivalent to a strictly stronger set-theoretic principlethan the one equivalent to Peano’s theorem (Simpson [1984],Theorems 3.9 and 4.2). The standard treatise on classical reversemathematics is (Simpson [1999/2009]).

Around the turn of this century, Veldman (see Other InternetResources), in the Netherlands, and Ishihara [2005, 2006], in Japan,independently initiated a programme ofconstructive reversemathematics (CRM), based on intuitionistic, rather thanclassical, logic. (Note, though, that the first published work in themodern era of CRM is probably that of Julian and Richman [1984], whichwas twenty years ahead of its time.) In this section of the article,we describe a less formal approach to CRM, in the style and frameworkof BISH. The aim of that CRM program is to classify the theorems inthe three standard models—CLASS, INT, and RUSS—accordingto which principles we must, and need only, add to BISH in order toprove them.

We stress that we restrict ourselves here toinformal CRM, inwhich we take for granted the principles of function- andset-construction described in the first chapters of Bishop [1967] orBishop & Bridges [1985], and we work in the informal, thoughrigorous, style of the practising analyst, algebraist, topologist,… .

In practice, CRM splits naturally into two parts. In the first ofthese, we consider a theorem \(T\) of INT or RUSS, and try to findsome principle, valid in that model and other than \(T\) itself, whoseaddition to BISH is necessary and sufficient for a constructive proofof \(T\). In the second part of CRM we deal with a theorem \(T\) ofCLASS that we suspect is nonconstructive, and we try to prove that\(T\) is equivalent, over BISH, to one of a number of knownessentially-nonconstructive principles, such as MP, LLPO, LPO, or LEM.For an example of this part of CRM, we mention our earlier proof thatthe classical least-upper-bound principle implies, and hence isequivalent to, LEM.

Incidentally, there is a strong argument for Brouwer [1921] being thefirst to deal with reverse-mathematical ideas: his Brouweriancounterexamples (see the one using the Goldbach conjecture, in Section1 above) lie squarely in the second part of CRM. Even if Brouwer didnot state those examples as logical equivalences, but as implicationsof the type

it is hard to believe that he was unaware that the right-hand-sideimplied the left in such cases.

5.1 Fan theorems in CRM

To illustrate the first part of CRM, we now concentrate on theorems ofthe type

where FT\(_?\) is some form of Brouwer’s fan theorem, and \(T\)is a theorem of INT. To do so, we need to distinguish between certaintypes of bar for thecomplete binary fan \(2^*\) (the set ofall finite sequences in \(\{0,1\})\).

Let \(\alpha \equiv (\alpha_1 ,\alpha_2, \ldots)\) be a finite orinfinite binary sequence. Theconcatenation of \(\alpha\)with another string \(\beta\) is

For \(b\) in \(\{0,1\}\) we write \(\alpha^{\frown}b\) rather than\(\alpha^{\frown}(b)\). By a \(\mathsf{c}\)-subset of \(2^*\)we mean a subset \(B\) of \(2^*\) such that

for some detachable subset \(D\) of \(2^*\). Every detachable subsetof \(2^*\) is a \(\mathsf{c}\)-subset. On the other hand, by a\(\Pi^{0}_1\)-subset of \(2^*\) we mean a subset \(B\) of\(2^*\) with the following property: there exists a detachable subset\(S\) of \(2^* \times \bN\) such that

and

Every \(\mathsf{c}\)-subset \(B\) of \(2^*\) is a\(\Pi^{0}_1\)-subset: simply take \(S = D \times \bN\), where \(D\) isa detachable subset of \(2^*\) such that (1) holds.

If \(?\) denotes a property of subsets of \(2^*\), thenBrouwer’sfan theorem for \(?\)-bars tells usthat every bar with the property \(?\) is a uniform bar. We areparticularly interested in the fan theorem for detachable bars(already discussed in Section 3.1):

FT\(_D\): Every detachable bar of the complete binary fan is uniform;

the fan theorem for \(\mathsf{c}\)-bars (that is, bars thatare \(\mathsf{c}\)-subsets):

FT\(_{\mathsf{c}}\): Every c-bar of the complete binary fan isuniform;

the fan theorem for \(\Pi^{0}_1\)-bars (that is, bars thatare \(\Pi^{0}_1\)-subsets):

FT\(_{\Pi^{0}_1}\): Every \(\Pi^{0}_1\)-bar of the complete binary fanis uniform;

and the full fan theorem:

FT: Every bar of the complete binary fan is uniform.

Note that, relative to BISH,

FT \(\Rightarrow\) FT\(_{\Pi^{0}_1} \Rightarrow\) FT\(_c \Rightarrow\)FT\(_D\).

Lubarsky and Diener [2014] have shown that these implications arestrict.

Typically, we want to prove that FT\(_?\) is equivalent, over BISH, tothe proposition that, for every set \(S\) of an appropriate sort, somepointwise property of the form

actually holds uniformly in the form

Our strategy for attacking this problem is two-fold. First, given aset \(S\) of the appropriate sort, we construct a ?-subset \(N\) of\(2^*\) such that

• if (2) holds, then \(B\) is a bar, and
• if \(B\) is a uniform bar, then (3) holds.

This, though, is only half of the solution. To prove that theimplication from (3) to (2) implies FT\(_?\), we consider a ?-subset\(B\) of \(2^*\) and construct a corresponding set \(S\) such that

• if \(B\) is a bar, then (2) holds, and
• if (3) holds, then \(B\) is a uniform bar.

The canonical example of such results is that of Julian and Richman[1984], in which \(S\) is the set of values of a given uniformlycontinuous mapping \(f : [0,1] \rightarrow \bR, T\) is the set ofpositive real numbers, and

The pointwise property we consider is

its uniform version being

The Julian-Richman results are as follows.

The proofs of these two theorems are subtle and tricky; see Julian& Richman [1984].

The two Julian-Richman theorems together reveal that, relative toBISH, the fan theorem FT\(_D\) is equivalent to thepositivityprinciple,POS:

Each positive-valued, uniformly continuous function on \([0,1]\) has apositive infimum.

It follows that POS is derivable in INT, in which the full fantheorem, not just FT\(_D\), is a standard principle. The situation isquiet the opposite in RUSS, where there exist both a detachable bar of\(2^*\) that is not uniform and a positive-valued, uniformlycontinuous function on \([0,1]\) that has infimum equal to 0; seeChapters 5 and 6 of Bridges & Richman [1987].

Berger and Ishihara [2005] have taken a different, indirect route toestablishing the equivalence of POS and FT\(_c\). They establish achain of equivalences between POS, FT\(_c\), and four principles ofthe type “if there is at most one object with property \(P\),then there is one such object”. The four unique-existenceprinciples are:

In, for example, the last of these, we say that a map \(f\) of ametric space \((X,\varrho)\) into itself

• has at most one fixed point if \(\varrho(f(x),x) +\varrho(f(y),y) \gt 0\) whenever \(\varrho(x,y) \gt 0\);
• has approximate fixed points if for each \(\varepsilon\gt 0\) there exists \(x \in X\) such that \(\varrho(f(x),x) \lt\varepsilon\).

A major open problem in CRM is that of finding a form of the fantheorem that is equivalent, over BISH, to theuniform continuitytheorem for \([0,1]\),

UCT\(_{[0,1]}\): Every pointwise continuous mapping of\([0,1]\) into \(\bR\) is uniformly continuous,

the proposition for which Brouwer originally developed his proof ofthe fan theorem. (Note that UCT\(_{[0,1]}\) is equivalent, relative toBISH, to the general uniform continuity theorem for metric spaces:Every pointwise continuous mapping of a complete, totally boundedmetric space into a metric space is uniformly continuous. See, forexample, Loeb [2005].)

It follows from results of Berger [2006] that

BISH \(\vdash\) UCT\(_{[0,1]}\Rightarrow\) FT\(_c\).

Also, Diener and Loeb (2008) have proved that

BISH \(\vdash\) FT\(_{\Pi^{0}_1} \Rightarrow\) UCT\(_{[0,1]}\).

However, we do not know if either of these implications can bereplaced by a bi-implication. Perhaps UCT\(_{[0,1]}\), and hence thefull uniform continuity theorem for compact metric spaces, isequivalent, relative to BISH, to some natural, but as yetunidentified, version of the fan theorem.

For additional material on the fan theorem in constructive reversemathematics, see, for example, Berger & Bridges [2007]; Diener[2008, 2012]; Diener & Loeb [2009]; and Diener & Lubarsky[2014]. In Dent [2013], there is a clear, though complex, diagramillustrating the interconnections between fan theorems, continuity,and omniscience principles (see Other Internet Resources).

Interested readers may pursue the topic of constructive reversemathematics in greater detail in the following supplementarydocument:

Ishihara’s principle \(\BDN\) and the anti-Specker Property

6. Constructive Algebra and Topology

Constructive mathematicians initially concentrated their efforts onthe field of analysis, with considerable success—witness thewealth of functional analysis developed in Bishop [1967]. This doesnot mean that, for example, algebra has been sidelined from theconstructive enterprise: the material in the monograph by Minesetal [1986] can be regarded as a substantial algebraic counterpartto the constructive analysis carried out by Bishop. Much morerecently, Lombardi and Quitté [2011] have published the firstlarge volume of a proposed two-volume work on constructive algebra.However, not being expert in algebra, and being aware of the danger ofmaking this article too long to hold the reader’s attention, wechoose not to discuss constructive analysis or algebra in any detail;rather, in the following supplementary document, we turn toconstructive topology, describing some rather different approaches tothat subject:

Approaches to Constructive Topology

7. Constructive Mathematical Economics and Finance

Investigations in constructive mathematical economics date back to aseries of papers on preference, utility, and demand from 1982 onwards;see Bridges [1999]. In his doctoral thesis, Hendtlass [2013]substantially weakened the conditions for the existence of a demandfunction; he also produced a wealth of results in fixed-point theoryand its applications, in particular to constructivisations of twoclassical proofs of the existence of an economic equilibrium.

In 2015, Berger and Svindland began a research project on constructivemathematical finance, at Ludwig-Maximilians-Universität inMunich.They first showed that the fundamental theorem on assetpricing, the separating hyperplane theorem, and Markov’sPrinciple are constructively equivalent (Berger & Svindland[2016]). Their more recent work has concentrated on how to circumventthe nonconstructivity of the classical extreme value theorem in orderto prove the existence of extreme points for functions in the presenceof even relatively weak convexity properties (Berger & Svindland[2016a]). Their project suggests that mathematical finance, likemathematical economics, may be a rich source of elegant, practicalconstructive theorems.

8. Concluding Remarks

The traditional route taken by mathematicians wanting to analyse theconstructive content of mathematics is the one that follows classicallogic; in order to avoid decisions, such as whether or not a realnumber equals 0, that cannot be made by a real computer, themathematician then has to keep within strict algorithmic boundariessuch as those formed by recursive function theory. In contrast, theroute taken by the constructive mathematician follows intuitionisticlogic, which automatically takes care of computationally inadmissibledecisions. This logic (together with an appropriate set- ortype-theoretic framework) suffices to keep the mathematics withinconstructive boundaries. Thus the mathematician is free to work in thenatural style of an analyst, algebraist (e.g., Mineset al.[1988]), geometer, topologist (e.g., Bridges &Vîță [2011], Sambin forthcoming), or other normalmathematician, the only constraints being those imposed byintuitionistic logic. As Bishop and others have shown, the traditionalbelief promulgated by Hilbert and still widely held today, thatintuitionistic logic imposes such restrictions as to render thedevelopment of serious mathematics impossible, is patently false:large parts of deep modern mathematics can be, and have been, producedby purely constructive methods. Moreover, the link betweenconstructive mathematics and programming holds great promise for thefuture implementation and development of abstract mathematics on thecomputer.

For further information about the state of modern constructivemathematics, we recommend the forthcomingHandbook of ConstructiveMathematics [Bridges et al., eds, 2023].

Bibliography

References

• Aberth, O., 1980,Computable Analysis, New York:McGraw-Hill.
• –––, 2001,Computable Calculus, NewYork: Academic Press.
• Bauer, A., 2005, “Realizability as the connection betweencomputable and constructive Mathematics”, Lecture notes for atutorial at a satellite seminar of CCA2005, Kyoto, Japan [available online].
• Beeson, M., 1985,Foundations of ConstructiveMathematics, Heidelberg: Springer Verlag.
• Berger, J., 2006, “The logical strength of the uniformcontinuity theorem”, inLogical Approaches to ComputationalBarriers, A. Beckmann, U. Berger, B. Löwe, and J. V. Tucker(eds.), Heidelberg: Springer Verlag.
• Berger, J., and Bridges, D.S., 2007, “A fan-theoreticequivalent of the antithesis of Specker’s theorem”,Proceedings of Royal Dutch Mathematical Society (IndagationesMathematicae) (Indag. Math. N.S.), 18(2): 195–202.
• –––, 2009, “The fan theorem andpositive-valued uniformly continuous functions on compactintervals”,New Zealand Journal of Mathematics, 38:129–135.
• Berger, J., and Ishihara, H., 2005, “Brouwer’s fantheorem and unique existence in constructive analysis”,Mathematical Logic Quarterly, 51(4): 360–364.
• Berger, J., and Schuster, P.M., 2006, “ClassifyingDini’s theorem”,Notre Dame Journal of FormalLogic, 47: 253–262.
• Berger, J., and Svindland, G., 2016, “A separatinghyperplane theorem, the fundamental theorem of asset pricing, andMarkov’s principle ”,Annals of Pure and AppliedLogic, 167: 1161–1170.
• –––, 2016a, “Convexity and constructiveinfima”,Archive for Mathematical Logic, 55:873–881.
• Bishop, E., 1967,Foundations of Constructive Analysis,New York: McGraw-Hill.
• –––, 1973,Schizophrenia in ContemporaryMathematics (American Mathematical Society Colloquium Lectures),Missoula: University of Montana; reprinted inErrett Bishop:Reflections on Him and His Research, American MathematicalSociety Memoirs 39.
• Bishop, E. and Bridges, D., 1985,Constructive Analysis,(Grundlehren der mathematischen Wissenschaften, 279), Heidelberg:Springer Verlag.
• Bourbaki, N., 1984,Éléments d’histoiredes mathématiques, Paris: Masson; English-languageedition,Elements of the History of Mathematics, J. Meldrum(trans.), 2006, Berlin: Springer Verlag.
• Bridges, D.S., 1999, “Constructive methods in mathematicaleconomics”, inZeitschrift fürNationalökonomie (Supplement), 8: 1–21.
• Bridges, D.S., and Diener, H., 2007, “The pseudocompactnessof [0, 1] is equivalent to the uniform continuitytheorem”,Journal of Symbolic Logic, 72(4):1379–1383.
• Bridges, D.S., and Richman, F., 1987,Varieties ofConstructive Mathematics, London Mathematical Society LectureNotes 97, Cambridge: Cambridge University Press.
• Bridges, D.S. and Vîță, L.S., 2006,Techniquesof Constructive Analysis, Heidelberg: Springer Verlag.
• –––, 2011,Apartness and Uniformity—AConstructive Development, Heidelberg: Springer Verlag.
• Bridges, D.S., Ishihara, H., Rathjen, M.J., and Schwichtenberg, H.(eds), forthcoming,Handbook of Constructive Mathematics,Cambridge: Cambridge University Press.
• Brouwer, L.E.J., 1907,Over de Grondslagen der Wiskunde,Doctoral Thesis, University of Amsterdam; reprinted with additionalmaterial, D. van Dalen (ed.), by Matematisch Centrum, Amsterdam,1981.
• –––, 1908, “De onbetrouwbaarheid derlogische principes”,Tijdschrift voor Wijsbegeerte, 2:152–158.
• –––, 1921, “Besitzt jede reelle Zahl eineDezimalbruchentwicklung?”,Mathematische Annalen, 83:201–210.
• –––, 1924, “Beweis, dass jede volleFunktion gleichmässig stetig ist”,Proceedings of RoyalDutch Mathematical Society, 27: 189–193.
• –––, 1924A, “Bemerkung zum Beweise dergleichmässigen Stetigkeit voller Funktionen”,Proceedings of Royal Dutch Mathematical Society, 27:644–646.
• Cederquist, J., and Negri, S., 1996, “A constructive proofof the Heine-Borel covering theorem for formal reals”, inTypes for Proofs and Programs (Lecture Notes in ComputerScience, Volume 1158), 62–75, Berlin: Springer Verlag.
• Constable, R.,et al., 1986,Implementing Mathematicswith the Nuprl Proof Development System, Englewood Cliffs, NJ:Prentice-Hall.
• Coquand, T., 1992, “An intuitionistic proof ofTychonoff’s theorem”,Journal of Symbolic Logic,57: 28–32.
• –––, 2009, “Space of valuations”,Annals of Pure and Applied Logic, 157: 97–109.
• –––, 2016, “Type Theory”,Stanford Encyclopedia of Philosophy (Winter 2016 Edition),Edward N. Zalta (ed.), URL = <https://plato.stanford.edu/entries/type-theory/>.
• Coquand, T., and Spitters, B., 2009, “Integrals andValuations”,Journal of Logic and Analysis, 1(3):1–22.
• Coquand, T., Sambin, G., Smith, J., and Valentini, S., 2003,“Inductively generated formal topologies”,Annals ofPure and Applied Logic, 124: 71–106.
• Curi, G., 2010, “On the existence of Stone-Čechcompactification”,Journal of Symbolic Logic, 75:1137–1146.
• Dent, J.E., 2013,Anti-Specker Properties in ConstructiveReverse Mathematics, Ph.D. thesis, University of Canterbury,Christchurch, New Zealand.
• Diaconescu, R., 1975, “Axiom of choice andcomplementation”,Proceedings of the American MathematicalSociety, 51: 176–178.
• Diener, H., 2008,Compactness under ConstructiveScrutiny, Ph.D. thesis, Christchurch, New Zealand: University ofCanterbury.
• –––, 2008a, “Generalisingcompactness”,Mathematical Logic Quarterly, 51(1):49–57.
• –––, 2012,“Reclassifying the antithesis ofSpecker’s theorem”,Archive for MathematicalLogic, 51: 687–693.
• Diener, H., and Loeb, I., 2009, “Sequences of Real Functionson [0, 1] in Constructive Reverse Mathematics”,Annals of Pure and Applied Logic, 157(1): 50–61.
• Diener, H., and Lubarsky, R., 2013, “Separating the fantheorem and its weakenings”, inLogical Foundations ofComputer Science (Lecture Notes in Computer Science, 7734), S.Artemov and A. Nerode (eds.), Berlin: Springer Verlag.
• Dummett, Michael, 1977 [2000],Elements of Intuitionism(Oxford Logic Guides, 39), Oxford: Clarendon Press, 1977; 2nd edition,2000. [Page references are to the 2nd edition.]
• Ewald, W., 1996,From Kant to Hilbert: A Source Book in theFoundations of Mathematics (Volume 2), Oxford: ClarendonPress.
• Feferman, S, 1975, “A language and axioms for explicitmathematics”, inAlgebra and Logit, J. N. Crossley(ed.), Heidelberg: Springer Verlag, pp. 87–139.
• –––, 1979, “Constructive theories offunctions and classes”, inLogic Colloquium ‘78,M. Boffa, D. van Dalen, and K. McAloon (eds.), Amsterdam: NorthHolland, pp. 159–224.
• Friedman, H., 1975, “Some systems of second order arithmeticand their use”, inProceedings of the 17th InternationalCongress of Mathematicians, Vancouver, BC, 1974.
• –––, 1977, “Set theoretic foundations forconstructive analysis”,Annals of Mathematics, 105 (1):1–28.
• Goodman, N.D., and Myhill, J., 1978, “Choice ImpliesExcluded Middle”,Zeitschrift für Logik und Grundlagender Mathematik, 24: 461.
• Hayashi, S., and Nakano, H., 1988,PX: A ComputationalLogic, Cambridge MA: MIT Press.
• Hendtlass, M., 2013,Constructing fixed points and economicequilibria, Ph.D. thesis, University of Leeds.
• Heyting, A., 1930, “Die formalen Regeln derintuitionistischen Logik”,Sitzungsberichte der PreussischeAkadademie der Wissenschaften. Berlin, 42–56.
• –––, 1971,Intuitionism—anIntroduction, 3rd edition, Amsterdam: North Holland.
• Hilbert, D., 1925, “Über das Unendliche”,Mathematische Annalen, 95: 161–190; translation,“On the Infinite”, by E. Putnam and G. Massey, inPhilosophy of Mathematics: Selected Readings, P. Benacerrafand H. Putnam (eds.), Englewood Cliffs, NJ: Prentice Hall, 1964,134–151.
• Hurewicz, W., 1958,Lectures on Ordinary DifferentialEquations, Cambridge, MA: MIT Press.
• Ishihara, H., 1992, “Continuity properties in constructivemathematics”,Journal of Symbolic Logic, 57 (2):557–565.
• –––, 1994, “A constructive version ofBanach’s inverse mapping theorem”,New Zealand Journalof Mathematics, 23: 71–75.
• –––, 2005, “Constructive Reversemathematics: compactness properties”, inFrom Sets and Typesto Analysis and Topology: Towards Practicable Foundations forConstructive Mathematics, L. Crosilla and P. Schuster (eds.),Oxford: The Clarendon Press.
• –––, 2006, “Reverse mathematics inBishop’s constructive mathematics”,PhilosophiaScientiae (Cahier Special), 6: 43–59.
• –––, 2013, “Relating Bishop’sfunction spaces to neighbourhood spaces”,Annals of Pure andApplied Logic, 164: 482–490.
• Johnstone, P.T., 1982,Stone Spaces, Cambridge: CambridgeUniversity Press.
• –––, 2003, “The point of pointlesstopology”,Bulletin of the American MathematicalSociety, 8: 41–53.
• Joyal, A., and Tierney, M., 1984, “An extension of theGalois theory of Grothendieck”,Memoirs of the AmericanMathematical Society, 309: 85 pp.
• Julian, W.H., and Richman, F., 1984, “A uniformly continuousfunction on [0, 1] that is everywhere different from itsinfimum”,Pacific Journal of Mathematics, 111:333–340.
• Kushner, B., 1985,Lectures on Constructive MathematicalAnalysis, Providence, RI: American Mathematical Society.
• Lietz, P., 2004,From Constructive Mathematics to ComputableAnalysis via the Realizability Interpretation, Dr. rer. nat.dissertation, Universität Darmstadt, Germany.
• Lietz, P., and Streicher, T., “Realizability models refutingIshihara’s boundedness principle”,Annals of Pure andApplied Logic, 163(12): 1803–1807.
• Loeb, I., 2005, “Equivalents of the (Weak) FanTheorem”,Annals of Pure and Applied Logic, 132:51–66.
• Lombardi, H., Quitté, C., 2011,AlgèbreCommutative. Méthodes constructives, Nanterre, France:Calvage et Mounet.
• Lorenzen, P., 1955,Einführung in die operative Logik undMathematik (Grundlehren der mathematischen Wissenschaften, Volume78), 2nd edition, 1969, Heidelberg: Springer.
• Lubarsky, R., and Diener, H., 2014, “Separating the FanTheorem and Its Weakenings”,Journal of Symbolic Logic,79(3): 792–813.
• Markov, A.A., 1954,Theory of Algorithms, Trudy Mat.Istituta imeni V.A. Steklova, 42, Moskva: Izdatel’stvo AkademiiNauk SSSR.
• Marquis, J.-P., “Category Theory”, 2015,The StanfordEncyclopedia of Philosophy (Winter 2015 Edition), Edward N. Zalta(ed.), URL = <https://plato.stanford.edu/archives/win2015/entries/category-theory/>.
• Martin-Löf, P., 1968,Notes on ConstructiveAnalysis, Stockholm: Almquist & Wiksell.
• –––, 1975, “An intuitionistic theory oftypes: predicative part”, inLogic Colloquium 1973,H.E. Rose and J.C. Shepherdson (eds.), Amsterdam: North-Holland.
• –––, 1980, “Constructive mathematics andcomputer programming”, inProc. 6th. Int. Congress forLogic, Methodology and Philosophy of Science, L. Jonathan Cohen(ed.), Amsterdam: North-Holland.
• –––, 1984,Intuitionistic Type Theory,Notes by Giovanni Sambin of a series of lectures given in Padova, June1980, Naples: Bibliopolis.
• –––, 2006, “100 years of Zermelo’saxiom of choice: what was the problem with it?”,TheComputer Journal, 49(3): 345–350.
• Menger, K., 1940, “Topology without points”,RiceInstitute Pamphlet, 27(1): 80–107 [available online].
• Mines, R., Richman, F., and Ruitenburg, W., 1988,A Course inConstructive Algebra, Universitext, Heidelberg: SpringerVerlag.
• Moerdijk, I., 1984, “Heine-Borel does not imply the fantheorem”,Journal of Symbolic Logic, 49(2):514–519.
• Moore, G.H., 2013,Zermelo’s Axiom of Choice: Its Origins,Development, and Influence, New York: Dover.
• Myhill, J., 1973, “Some Properties of IntuitionisticZermelo-Fraenkel Set Theory”, inCambridge Summer School inMathematical Logic, A. Mathias and H. Rogers (eds.), LectureNotes in Mathematics, 337, Heidelberg: Springer Verlag, 206–231.
• –––, 1975, “Constructive SetTheory”,Journal of Symbolic Logic, 40(3):347–382.
• Naimpally, S., 2009,Proximity Approach to Problems inTopology and Analysis, Munich: Oldenbourg Verlag.
• Naimpally, S., and Warrack, B.D., 1970,Proximity Spaces(Cambridge Tracts in Math. and Math. Phys., Volume 59), Cambridge:Cambridge University Press.
• Nordström, B., Peterson, K., and Smith, J.M., 1990,“Programming in Martin-Löf’s Type Theory”,Oxford: Oxford University Press.
• Palmgren, E., 2007, “A constructive and functorial embeddingof locally compact metric spaces into locales”,Topology andits Applications, 154: 1854–1880.
• –––, 2008, “Resolution of the uniformlower bound problem in constructive analysis”,MathematicalLogic Quarterly, 54: 65–69.
• –––, 2009, “From intuitionistic to formaltopology: some remarks on the foundations of homotopy theory”,in:Logicism, Intuitionism and Formalism—what has become ofthem?, S. Lindström, E. Palmgren, K. Segerberg, and V.Stoltenberg-Hansen (eds.), 237–253, Berlin: SpringerVerlag.
• Petrakis, I., 2016, “A constructive function-theoreticapproach to topological compactness”, inLogical Methods inComputer Science 2016, IEEE Computer Society Publications:605–614.
• –––, 2016a, “The Urysohn Extension Theoremfor Bishop Spaces”, in S. Artemov and A. Nerode (eds.),Symposium on Logical Foundations in Computer Science 2016(Lecture Notes in Computer Science 9537), Berlin: Springer Verlag,299–316.
• Picado, J., and Pultr, A., 2011,Frames and Locales: Topologywithout Points, Basel: Birkhäuser Verlag.
• Richman, F., 1983, “Church’s Thesis WithoutTears”,Journal of Symbolic Logic, 48:797–803.
• –––, 1990, “Intuitionism asgeneralization”,Philosophia Mathematica, 5:124–128.
• –––, 1996, “Interview with a constructivemathematician”,Modern Logic, 6: 247–271.
• –––, 2000, “The Fundamental Theorem ofAlgebra: A Constructive Treatment Without Choice”,PacificJournal of Mathematics, 196: 213–230.
• Riesz, F., 1908, “Stetigkeitsbegriff und abstrakteMengenlehre”,Atti IV Congresso Internationale MatematicaRoma II, 18–24.
• Sambin, G., 1987, “Intuitionistic formal spaces—afirst communication”, inMathematical Logic and itsApplications, D. Skordev (ed.), 187–204, New York: PlenumPress.
• –––, forthcoming,The Basic Picture:Structures for Constructive Topology, Oxford: Oxford UniversityPress.
• Sambin, G., and Smith, J. (eds.), 1998,Twenty Five Years ofConstructive Type Theory, Oxford: Clarendon Press.
• Schuster, P.M., 2005, “What is continuity,constructively?”,Journal of Universal ComputerScience, 11: 2076–2085
• –––, 2006, “Formal Zariski topology:positivity and points”,Annals of Pure and AppliedLogic, 137: 317–359.
• Schwichtenberg, H., 2009, “Program extraction inconstructive analysis”, inLogicism, Intuitionism andFormalism—what has become of them?, S. Lindström, E.Palmgren, K. Segerberg, and V. Stoltenberg-Hansen (eds.), Berlin:Springer Verlag, 255–275.
• Simpson, S.G., 1984, “Which set existence axioms are neededto prove the Cauchy/Peano theorem for ordinary differentialequations”,Journal of Symbolic Logic, 49(3):783–802.
• –––, 2009,Subsystems of Second OrderArithmetic, second edition, Cambridge: Cambridge UniversityPress.
• Specker, E., 1949, “Nicht konstruktiv beweisbare Sätzeder Analysis”,Journal of Symbolic Logic, 14:145–158.
• Steinke, T.A., 2011,Constructive Notions of Compactness inApartness Spaces, M.Sc. Thesis, University of Canterbury,Christchurch, New Zealand.
• Troelstra, A.S., 1978, “Aspects of ConstructiveMathematics”, inHandbook of Mathematical Logic, J.Barwise (ed.), Amsterdam: North-Holland.
• Troelstra, A.S., and van Dalen, D., 1988,Constructivism inMathematics: An Introduction (two volumes), Amsterdam: NorthHolland.
• van Atten, M., 2004,On Brouwer, Belmont:Wadsworth/Thomson Learning.
• van Dalen, D., 1981,Brouwer’s Cambridge Lectures onIntuitionism, Cambridge: Cambridge University Press.
• –––, 1999,Mystic, Geometer andIntuitionist: The Life of L.E.J. Brouwer (Volume 1), Oxford:Clarendon Press.
• –––, 2005,Mystic, Geometer, andIntuitionist: The Life of L.E.J. Brouwer (Volume 2), Oxford:Clarendon Press.
• van Stigt, W.P., 1990,Brouwer’s Intuitionism,Amsterdam: North-Holland.
• Vickers, S., 2005, “Localic completion of generalized metricspaces I”,Theory and Applications of Categories,14(15): 328–356.
• Waaldijk, F., 2005,On the foundations of constructivemathematics,Foundations of Science, 10(3):249–324.
• Wallman, H., 1938, “Lattices of topological spaces”,Annals of Mathematics, 39: 112–126.
• Weihrauch, K., 2000,Computable Analysis (EATCS Texts inTheoretical Computer Science), Heidelberg: Springer Verlag.
• Weyl, H., 1946, “Mathematics and Logic”,AmericanMathematical Monthly, 53(1): 2–13.
• Whitehead, A.N., 1919,An Enquiry Concerning the Principles ofNatural Knowledge, Cambridge: Cambridge University Press, secondedition, 1925.

Related Literature

• Heijenoort, Jean van, 1967,From Frege to Gödel: A SourceBook in Mathematical Logic 1879–1931, Cambridge, MA:Harvard University Press.
• Hilbert, David, 1928, “Die Grundlagen der Mathematik”,Hamburger Mathematische Einzelschriften 5, Teubner, Leipzig. Reprintedin English translation in van Heijenoort 1967.

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

• The Agda Wiki, a typed functional programming language and proof assistant,Göteborg University and Chalmers University of Technology.
• Agda, entry in Wikipedia.
• The Coq Proof Assistant, Inria, 1984–2017.
• Coq, entry in Wikipedia.
• James Dent’s Diagram.
• Bauer, A., 2005, “Realizability as the connection between computable and constructive mathematics”.
• Veldman, W., 2014, “Brouwer’s Fan Theorem as an Axiom and as a Contrast to Kleene’s Alternative”, arxiv:1106.2738https://arxiv.org/abs/1106.2738.

Related Entries

Brouwer, Luitzen Egbertus Jan |logic, history of: intuitionistic logic |logic: intuitionistic |mathematics, philosophy of |mathematics, philosophy of: intuitionism |set theory: constructive and intuitionistic ZF |type theory: intuitionistic

Acknowledgments

Bridges thanks Philip Catton for kindly advising him about an earlyversion of this entry; Fred Richman, the late Ray Mines, Bill Julian,Hajime Ishihara, Helmut Schwichtenberg, and Peter Schuster, fordecades of friendship, mathematical collaboration, and support duringvisits to their institutions; Luminita Vîţă, HannesDiener, Matt Hendtlass, Maarten McKubre-Jordens, Josef Berger, IrisLoeb, and many other students, postdocs, and colleagues, for theirparticipation in the constructive programme; the University ofBuckingham, England, for giving him opportunity and encouragement atthe start of his academic career; and the Universities of Waikato andCanterbury, for supporting him in New Zealand since 1989. Last, butnot least, he thanks Hajime Ishihara for stepping into the authorialbreach made by the untimely death of Erik Palmgren.