Could not include mathematicscontents
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.
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.
Brouwer never accepted a complete axiomatisation of intuitionistic mathematics. However, we can identify several principles, which may not (even historically) be complete.
There's also some stuff about choice sequences that I don't really understand.
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.
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.
The roots of Brouwer’s intuitionism are apparently in his PhD thesis
Then an axiomatization of intuitionistic mathematics is given in
General reviews include
Stanford Encyclopedia of Philosophy, Intuitionism in the Philosophy of Mathematics Reviews with further developments include for instance
(with a focus on constructive analysis).
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 below:
General comments on intuitionistic mathematics/logic as the natural language for physics are in