# nLab intuitionistic mathematics

foundations

## Foundational axioms

foundational axiom

## Removing axioms

#### Constructivism, Realizability, Computability

intuitionistic mathematics

# Intuitionistic mathematics

## Idea

Intuitionistic mathematics is a variety of constructive mathematics done according to the principles accepted by L.E.J. Brouwer and his philosophy of intuitionism.

## Terminology

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’:

• Intuitionism is an early-20th-century philosophy of mathematics developed by Brouwer, according to which mathematics is a free creation of a mind, and valid results are about what that mind creates (rather than about an external reality, as in platonism, or about nothing, as in formalism). From this very controversial starting point, Brouwer developed a style of mathematics and even logic, which he saw as derived from mathematics (rather than conversely, as in logicism?). Intuitionism is one particular philosophy of constructivism.

• Intuitionistic mathematics is the mathematics that Brouwer came up with. However, it's not necessary to accept Brouwer's philosophy to practise intuitionistic mathematics; conversely, one may accept Brouwer's philosophical starting place but not his conclusions about the resulting mathematics. Intuitionistic mathematics is one particular variety of constructive mathematics.

One example of intuitionistic mathematics (which nicely shows that intuitionism is not a matter of “belief” but of subject) is computable mathematics (see for instance Bauer 05, section 4.3.1).

• Intuitionistic set theory? is a set theory, generally proffered as a foundation of mathematics, intended to capture intuitionistic mathematics. As the terminology is usually used (for example in the name of IZF, intuitionistic Zermelo-Frankel set theory?), ‘intuitionistic’ means that excluded middle fails but power sets are included (making it impredicative). In contrast, ‘constructive’ set theory (such as CZF, constructive Zermelo-Frankel set theory?) has function sets but not power sets (making it weakly predicative). The former is technically convenient, but the latter is better motivated. That said, both are less predicative than Brouwer's mathematics.

• Intuitionistic type theory is generally proffered as a foundation of mathematics, which is usually predicative. For purposes of comparing type theory to set theory, it might be nice if ‘intuitionistic’ and ‘constructive’ were distinguished for type theories as they are for set theories, but they aren't. (Then again, there was never much sense in that distinction for set theories, or at least not for making it using that terminology.)

• Intuitionistic logic is the logic that intuitionistic mathematics, set theory, and type theory use, which lacks the principle of excluded middle; other forms of constructive mathematics also use intuitionistic logic, which is also known as constructive logic.

## Mathematical principles

Brouwer never accepted a complete axiomatisation of intuitionistic mathematics. However, we can identify several principles, which may not (even historically) be complete.

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.

## 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.

## References

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

• L.E.J. Brouwer, Over de Grondslagen der Wiskunde, PhD thesis, Universiteit van Amsterdam, 1907.

Then an axiomatization of intuitionistic mathematics is given in

• Stephen Kleene, R. E. Vesley, The foundations of intuitionistic mathematics,North-Holland (1965)

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

General reviews include