basic constructions:
strong axioms
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
Could not include mathematicscontents
Intuitionistic mathematics is a variety of constructive mathematics done according to the principles accepted by L.E.J. Brouwer and his philosophy of intuitionism.
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.
Brouwer never accepted a complete axiomatisation of intuitionistic mathematics. However, we can identify several principles, which may not (even historically) be complete.
In hindsight, we may say that inuitionistic mathematics is done in a pretopos identified as Set.
We have the axiom of infinity and countable choice, as in classical mathematics.
We have the classically false principles of continuity? and continuous choice?.
We have the fan theorem and bar theorem?, which are classically true but fail in Russian constructivism.
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.
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.
The roots of Brouwer’s intuitionism are apparently in his PhD thesis
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 reviews include
Stanford Encyclopedia of Philosophy, Intuitionism in the Philosophy of Mathematics Reviews with further developments include for instance
Frank Waaldijk, On the foundations of constructive mathematics – especially in relation to the theory of continuous functions (pdf)
(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
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.