nLab
intuitionistic mathematics

Context

Foundations

Constructivism, Realizability, Computability

Mathematics

Intuitionistic mathematics

Idea

Intuitionistic mathematics (often abbreviated INT) is the earliest full-blown variety of constructive mathematics, done according to the mathematical principles developed by L.E.J. Brouwer through his philosophy of intuitionism.

Beware that this terminology is not consistent across mathematics. Not infrequently the word “intuitionistic” is used to refer simply to constructive mathematics in general, or to constructive logic, or to impredicative set theory done in constructive logic. This page is about Brouwer’s intuitionism, which is a specific variety of constructive mathematics that (unlike “neutral” constructive mathematics) uses axioms that contradict classical mathematics. For more on this see at Terminology below.

The first main philosophical idea is that mathematical truth (a true statement) can only be attained in one’s mind, by carefully arranging one’s concepts and constructions in such a way that there remains absolutely no doubt that every aspect of the statement is verified, unambiguously, without reliance on any ‘outside’ assumption, for instance about the platonic nature of reality. (The principle of excluded middle is such an assumption, and Brouwer gave mathematical counterexamples to its validity, eventually leading to the foundational crisis in mathematics (Grundlagenstreit) around 1930, and Brouwer’s conflict with Hilbert).

The second main philosophical idea is that the mind works over time. One does not have everything ready and done from the start. Infinity is a (perceived) idealized property of time, but one cannot have completed any infinite process or construction on any given day. Infinity is potential, not actual.

The main mathematical idea then becomes that we can only build mathematical structures and truths starting from the natural numbers 0,1,...0, 1, ... (where the dots indicate potential, not actual infinity). Natural numbers are definite and precise, but most real numbers, such as π\pi, have a very different nature. We can only form something that we call ‘π\pi’ through a never-finished process of approximation.

Nonetheless, a substantial part of mathematics can be built up (‘constructed’) in this way. What mainly differentiates intuitionistic mathematics from constructive mathematics are two added axioms.

Brouwer ‘deduced’ two axiomatic insights, notably ‘continuous choice’ and a transfinite-induction based knowledge principle called `the Bar Theorem'. 'Continuous choice' conflicts with classical mathematics, the Bar Theorem is classically true (it boils down to stating that any open cover of Baire space is inductive).

Kleene & Vesley (in Foundations of Intuitionistic Mathematics, 1965) offered a clean axiomatic approach which is nowadays called FIM. Kleene proved that FIM is equiconsistent with classical mathematics. Kleene also proved that theorems of FIM are recursively realizable, which shows the computational content of FIM.

Terminology

Terminological ambiguity is often present in constructive mathematics and its varieties. Intuitionistic mathematics (INT) includes axioms that contradict classical logic; but people in non-foundational disciplines often use “intuitionistic” to mean roughly the same as “constructive mathematics” (say: mathematics without the principle of excluded middle, usually with computational/algorithmic content and some restriction on impredicativity, but nothing added that contradicts classical mathematics).

There are a variety of ways to use the term ‘intuitionistic’. We list them here, roughly from the most specific to the most general, and contrast (where appropriate) with the term ‘constructive’:

There is variant of the NuPrl type theory with choice sequences: PDF.

Mathematical principles

Brouwer did not believe in a rigourous formalization of mathematics, for various reasons (amongst which the mathematical incompleteness of formal systems, as later proved by Gödel's incompleteness theorem). He saw mathematical logic and formal systems as a correct part of mathematics, but held that this part could capture the essence nor the scope of mathematics in a meaningful way. Nonetheless he admitted that certain often-used arguments and mental constructions could be formalized `as an abbreviation'.

Brouwer’s student Arend Heyting (who later succeeded Brouwer as professor in Amsterdam) formalized what is now known as intuitionistic logic. He also is largely responsible for the Brouwer-Heyting-Kolmogorov interpretation (BHK) of intuitionistic logic, BHK can be seen as a precursor to realizability.

Although it's not enough to derive all of the above, much of the essence of intuitionistic mathematics, or at least intuitionistic analysis, can be summarized in the theorem that every (set-theoretic) function from the unit interval to the real line is uniformly continuous.

Intuitionistic mathematics is often regarded as a specialization of Bishop's constructive mathematics obtained by adding the above principles, but this is somewhat questionable if it refers to what Bishop actually did (and in particular the fact that he worked with Bishop sets); see Bishop's constructive mathematics for discussion.

Feel

In intuitionistic mathematics, already set theory behaves a lot like topology, a point stressed by Frank Waaldijk (web). He uses the Kleene-Vesley? system. Fourman’s continuous truth makes this remark precise using topos theory.

Although intuitionistic mathematics does not accept all function sets (much less power sets), it seems to allow for both inductive and coinductive structures; see a Café comment. The reluctance to add function spaces is similar to the problem of function spaces in topology; see nice category of spaces.

References

For more see also the references at constructive mathematics.

The roots of Brouwer’s intuitionism are apparently in his PhD thesis

A reference written by Brouwer and still in print in English is

Early exposition and endorsement:

Then an axiomatization of intuitionistic mathematics is given in

in terms of realizability (the Kleene-Vesley topos), and hence intuitionistic mathematics is shown to be consistent.

General review:

Reviews with further developments:

Discussion of an approach to general topology in intuitionistic mathematics: