basic constructions:
strong axioms
noncommutative geometry (general flavour)
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 from the most specific to the most general:
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 starting point, Brouwer developed a very controversial style of mathematics and even logic, which he saw as derived from mathematics (rather than conversely, as in logicism?).
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 logic is the logic that Brouwer's mathematics uses, which lacks the principle of excluded middle. However, there are many other styles of mathematics that also use intuitionistic logic; these are known more generally as constructive mathematics.
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 sequence?s that I don't really understand.
Although it's not enough to derive all of the above, much of the essence of intuitionistic mathematics can be summarised 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).
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.