nLab
intuitionistic mathematics

Context

Foundations

Constructivism, Realizability, Computability

Mathematics

Could not include mathematicscontents

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 intuitionstic 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

For more see also the references at constructive mathematics.

That computable mathematics is an incarnation of intuitionistic mathematics is spelled out in the lecture notes

  • Andrej Bauer, around section 4,3.1 in 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)

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.

Revised on May 3, 2014 02:47:00 by Frank Waaldijk (31.151.247.133)