nLab constructive mathematics

Constructive mathematics

Context

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Mathematics

Constructivism, Realizability, Computability

Constructive mathematics

Idea

Broadly speaking, constructive mathematics is mathematics done without the principle of excluded middle, or other principles, such as the full axiom of choice, that imply it, hence without “non-constructive” methods of formal proof, such as proof by contradiction. This is in contrast to classical mathematics, where such principles are taken to hold.

There are variations of what exactly is regarded as constructive mathematics, for instance intuitionism or predicativism, see the list of schools below. But beware the ambiguity in terminology: In Brouwer-style intuitionistic mathematics one includes axioms that contradict classical logic, while other authors use “intuitionistic” to mean what elsewhere is called “constructive”, and referring only to rejection of excluded middle and choice. Some authors (particularly material set theorists) use “constructive” to mean predicative constructive and “intuitionistic” to mean impredicative constructive. Other authors emphasize the necessity that constructive theories be proof relevant, with denial of the excluded middle’s universality subordinate to this requirement; see (Harper 2013).

Constructivism is the philosophy that such mathematics is useful, or (more strongly) that non-constructive mathematics is wrong. Historically, constructive mathematics was first pursued explicitly by mathematicians who believed the latter. However, many modern mathematicians who do constructive mathematics do it not because of any philosophical belief about the wrongness of non-constructive mathematics, but because constructive mathematics is interesting in its own right. In the ‘pluralist’ approach to the foundations of mathematics, a constructive proof (when it exists) is better because it is valid in more versions of mathematics, but a classical proof remains valid for classical mathematics.

Another motivation for modern mathematicians —especially category theorists like those on the nLab— is that the study of constructive mathematics has potential applications to non-constructive mathematics. For example, even if one believes the principle of excluded middle to be true, the “internal” version of excluded middle in many interesting categories is still false; thus constructive mathematics can be useful in the study of such categories, even if mathematics is “globally” non-constructive. This is the neutral motivation for constructive mathematics from the nPOV.

Here we write mostly about the mathematics, trying to be mostly neutral philosophically.

Origins and schools

During the “foundational crisis” in mathematics around the beginning of the 20th century, a number of mathematicians espoused philosophies that are generally grouped together and labeled constructivist. The common feature of these philosophies was a rejection of axioms and principles of logic that lead to nonconstructive proofs. There was much talk at the time about potential vs absolute infinity, but from an axiomatic perspective, it turns out that (if one stops short of finitism) the two main culprits are

Thus, constructivists (including many still active today) reject proofs that make use of either of these. (In fact, it was realized in 1975 by Diaconescu that the axiom of choice implies the principle of excluded middle. Excluded middle is precisely the “finitely indexed” axiom of choice; see excluded middle for a proof.)

There are, however, differences among constructivists as well, even discounting the pluralists.

Many constructivists (like many classical mathematicians) believe in an absolute mathematical sense of “truth,” and that in this sense choice and excluded middle are simply wrong. (Some constructivists, using classically false axioms, can even refute them; others merely claim that no possible correct reasoning could ever prove them. See Truth versus assertability below.) To most mathematicians, this makes them seem quite strange. Other constructivists adopt a wait-and-see attitude, or even a relative notion of truth (which can seem strange in another way).

The following is a partial list of schools and subtheories of constructive mathematics:

Topos theory

With the invention of topos theory in the second half of the 20th century, a new sort of constructivism arose. It was observed (by Lawvere and others) that any topos with a natural numbers object has an internal logic which is powerful enough to interpret most of mathematics, but that this logic in general fails to satisfy choice and excluded middle. This meant that even for a mathematican who likes to use choice and excluded middle (and a fortiori for one who believes them to be “true”), there is a reason to care about what can be proven without them, because only if a proof is constructive can it be interpreted in an arbitrary topos with NNO.

Even starting from a “completely classical” world of mathematics, many interesting toposes arise naturally (such as the category of sheaves on any topological space, or more generally any site) whose internal logic is not classical logic. Then by internal reasoning in such a topos (which is constructive reasoning), one can prove various useful facts, which can then be reinterpreted as external statements about the behavior of the topos itself. For example, the constructive theorem that every one-sided real number that is both a lower real and an upper real must be located (which, classically, is an utter triviality) becomes the theorem that any semicontinuous function (from any topological space to the real line) that is both upper and lower semicontinuous must be continuous (which is at least somewhat nontrivial).

By now it is known that many of the non-classical axioms used by the early constructivists have natural models in particular toposes. For instance, in the topos of sheaves on the real numbers RR, the continuity axiom? that “all total functions RRR \to R are continuous” holds. And in the effective topos, the computability axiom? that “all partial functions NNN\to N are computable” holds.

However, there are no non-classical (or classical) axioms beyond “pure constructivism” that are true in all toposes with NNO. In particular, there is a free topos with NNO such that a statement is true in the free topos precisely when it is provable in pure (Richman-school) constructive mathematics. This means that for an argument to apply in all toposes, even mild assumptions such as countable or dependent choice are unacceptable (but impredicativity is fine). However, topos theory has also provided ideas that solve many of the problems with pure constructivism. For example, a well-behaved notion of “continuous function” can be recovered by using locales instead of topological spaces, which was first discovered in the context of toposes and is closely related to them in any case.

Some features of constructive mathematics

Rephrasing of classical ideas

Sometimes, all that is necessary to make a piece of mathematics constructive is careful use of language. It is common in classical mathematics to define things with an unnecessary amount of negation. This doesn’t work so well constructively, since a statement can be not false without being true, but we can sometimes do perfectly well by just removing unnecessary double negations.

For example, classically one often speaks about “nonempty” sets, meaning a set which “does not have no elements.” Constructively it is much better to say that a set “does have at least one element”; constructivists often call such a set inhabited to remind themselves that it is a “positive” notion to replace the negative one of “nonempty”. Others continue to use the word “non-empty” but understand it as a term of art that really means “inhabited”.

Bifurcation of notions

On the other hand, differences in axiomatization or definition that make no difference classically can result in actual differences in behavior constructively. Therefore, classically equivalent notions often “bifurcate” (or “trifurcate” or worse) into multiple inequivalent constructive ones. This tends to happen whenever a concept involves negation and, to a lesser degree, disjunction and existential quantification. In some cases there is a “correct” constructive version of the definition, although it may take some thought to uncover it, but in many cases more than one of the resulting concepts is important and useful. For example:

  • There are multiple inequivalent constructive definitions of a field, because of the axioms “every nonzero element has an inverse” and 010 \neq 1.

  • In pure constructive logic, there are multiple inequivalent definitions of real numbers.

  • There are at least three different constructive notions of ordinal number; see (Taylor 1996) and (Joyal–Moerdijk 1995).

  • Without the axiom of choice, functors and anafunctors become distinct, and often the latter is more appropriate; see (Makkai, 1996).

  • Perhaps most disturbingly of all to the classical mathematician, one must distinguish between finite sets, subfinite sets, finitely-indexed sets, and even subfinitely indexed sets; see finite set for definitions. However, in practice it is usually either finite or finitely-indexed sets that are important, and with practice a little bit of thought suffices to show which is the relevant concept.

Negative translation

This allows one to translate classically valid theorems into intuitionistically valid theorems. See double negation translation.

Truth versus assertability

Already in classical mathematics, there is a difference between saying that something is true and saying that something is provable. If you adopt ZFC because you believe it correct, then presumably you believe that ZFC is consistent even though (assuming that you're aware of certain theorems) you also know that you cannot prove it so. In that case, you also believe that the continuum hypothesis (for example) is either true or false; you may or may not have an opinion on which it is, but in any case again you know that you cannot prove it either way.

A constructive mathematician can be even subtler. If you belong to the Bishop school, then you accept no classically false axioms, and anything that you can prove is valid also in classical mathematics. Even so, you can believe that the principle of excluded middle is false (even though, of course, you know that you cannot prove it false). So you can really confuse the classical mathematicians by saying, on the one hand, that they can safely accept all of your theorems as valid, and then saying, on the other hand, that you know excluded middle to be false. The resolution, of course, is that you never claimed that this was a theorem.

This way of talking has even been formalised in (Bishop, 1967) with a convention adopted by many (but not all) of his followers. In this convention, the word ‘not’, used normally in a vernacular sentence whose mathematical content would otherwise be the proposition pp, changes to the content to ¬p\neg p, or pp \to \bot, as usual. (This follows all of the rules of intuitionistic logic; in particular, any statement that is ‘not’ true is false (just as in classical logic).) However, the word ‘not’, in italics as shown here, changes the content to pxp \to x, where xx is some statement that is known (although not proved!), according to Bishop, to be false. Now a statement that is ‘not’ true may be false, but this may be unknown, and it is even possible that it is also ‘not’ false (so ¬px\neg p \to x, possibly for a different xx).

Bishop gives in his introduction several statements, suitable for use as xx above, including:

  • excluded middle itself, which Bishop call the ‘principle of omniscience’;
  • the ‘limited principle of omniscience’: any infinite sequence in {0,1} N\{0,1\}^N is either all 00 or has at least one 11;
  • the ‘lesser limited principle of omniscience’: for any two infinite sequence in {0,1} N\{0,1\}^N that do not both have at least one 11, at least one of these sequences does not have at least one 11;
  • others.

At one point in his book, while discussing the possibility of a pointwise-continuous function [0,1]R[0,1] \to R that is not uniformly continuous (a Specker function?, whose existence Markov's school claims as a theorem), Bishop seems to assert that this theorem is both not true and not false; he does not put it this way, so this may not be exactly what he meant, but there is no contradiction if it is. (But it is a contradiction, even in intuitionistic logic, if a statment is both not true and not false; indeed, a definition of ‘false’ may be taken to be ‘not true’.)

This practice can be understood through a careful distinction between object language and metalanguage. A mathematical statement pp (such as the continuum hypothesis, or that a Specker function exists) belongs to the object language, as does ¬p\neg p or pxp \to x for any specific mathematical statement xx. But the statement that pp is provable in some formal system belongs to the metalanguage (although it can also phrased internal to any object language suitable for mathematics), and as such may be written p\vdash p. The metalanguage has its own logic (the metalogic, which for the sake of argument we may even assume to be classical), but notice that ¬p\neg \vdash p and ¬p\vdash \neg p are different; the first claims that pp cannot be proved, while the second claims that pp can be refuted, which (in any consistent? formal system, even a classical one) is strictly stronger. Although Bishop did not commit to any formal system, if we assume for the sake of argument that he settled on one, then we may write ¬p\vdash \neg p as our interpretation of his meaning when he asserts ‘not pp’ but ¬p\neg \vdash p as his meaning when he asserts ‘not pp’.

Even without the notational convention of the Bishop school, it is important when reading constructive mathematics to remember the difference between what can be refuted (proved false) and what merely cannot be proved true. Although Brouwer's and Markov's schools will sometimes claim to prove statements that are (classically) outright false (such as that every function [0,1]R[0,1] \to R is pointwise-continuous), it is more common (and can happen in any school) that a constructive mathematician makes a claim that merely sounds false, when what they really mean is only that they don't accept what you say as true. Often modal phrases like ‘not necessarily’ will be used where Bishop would use ‘not’, as a clue that we're shifting to a metalanguage, or at least merely remaining agnostic rather than outright disagreeing.

The distinction between object language and metalanguage exists even in classical mathematics, but it seems that most classical mathematicians are not used to remembering it, although it is not entirely clear why this should be so. One possibly relevant observation is that even if PP is a statement which is neither provable nor disprovable (like the continuum hypothesis), in classical mathematics it is still provable that “PP is either true or false.” Moreover, classical model theory often restricts itself to two-valued models? in which the only truth values are “true” and “false,” although classical logic still holds in Boolean-valued models, and in such a case the truth value of PP may be neither “true” nor “false,” although the truth value of “PP or not PP” is still “true.” Certainly when talking about classical truths which fail constructively, such as excluded middle, it is important to remember that “fails to be provable” is different from “is provably false.”

Prehistory

In

the following comment about mathematical proof (in section 12 Historical and mathematical proof of the Preface) might be read as being a complaint about the traditional non-constructive concept of proof and about the traditional lack of proof relevance:

All the same, while proof is essential in the case of mathematical knowledge, it still does not have the significance and nature of being a moment in the result itself; the proof is over when we get the result, and has disappeared. The process of mathematical proof does not belong to the object; it is a function that takes place outside the matter in hand.

footnote 42: Mathematical truths are not thought to be known unless proved true. Their demonstrations are not, however, kept as parts of what they prove, but are only our subjective means towards knowing the latter. In philosophy, however, consequences always form part of the essence made manifest in them, which returns to itself in such expressions.

See also earlier conceptions of proofs expressing the ‘cause’ of a theorem, where reductio proofs in particular were taken generally to fail. Such an idea goes back to Aristotle for whom a proper answer to the question “Why is the angle in a semicircle a right-angle?” gives its cause.

  • Paolo Mancosu, Philosophy of Mathematics and Mathematical Practice in the Seventeenth Century, OUP, 1996.

See also

Concepts that usually arise in constructive mathematics, often because they are classically trivial:

Some of these are also useful internally or even classically.

Topics relevant to the foundations of constructive mathematics:

Other articles with content relating to constructive mathematics (rather incomplete):

In principle, every article could explain how it applies to constructive mathematics, but that will probably never happen.

There is also

  • constructivism and idealism?

References

See also the references at intuitionistic mathematics for more.

Original texts:

rewritten as:

Early monographs:

Gentle introductions:

An more technical introduction to constructive reasoning in mathematics is (with an eye towards homotopy type theory) in the introduction of:

Other accounts:

In view of reverse mathematics:

General comments on intuitionistic mathematics/logic as the natural language for physics are in

For more on physics formalized in intuitionistic mathematics (notably in topos theory) see at geometry of physics.

For an emphasis on proof relevance, see:

Most books on topos theory include some discussion of toposes' internal constructive logic. One good reference is:

A historical account is in

The relation to realizability and computability is discussed in

  • Andrej Bauer, Realizability as connection between constructive and computable mathematics, in T. Grubba, P. Hertling, H. Tsuiki, and Klaus Weihrauch, (eds.) CCA 2005 - Second International Conference on Computability and Complexity in Analysis, August 25-29,2005, Kyoto, Japan, ser. Informatik Berichte, vol. 326-7/2005. FernUniversität Hagen, Germany, 2005, pp. 378–379. (pdf)

On commutative algebra with constructive methods:

Last revised on January 28, 2024 at 05:26:29. See the history of this page for a list of all contributions to it.