[xelxebar]

I'm not sure the original paper has enough substance to precisely pin down the author's preferred axioms. In practice, the adjectives "intuitionistic" and "constructive" are used with enough author-specific meanings that you just need to read their definition each time.

FWIW, the term "intuitionistic mathematics" sounds a bit odd to my ear. Usually you hear about "intuitionistic logic" or "constructive logic" which are both part of the larger program of "constructive mathematics."

Anyway, the "Five Stages" paper I link does a good job of introducing the broader ideas of constructive mathematics and, perhaps, gives a taste of what Gisin is excited about.

> The equations of physical models and their solution stays exactly the same in constructive mathematics as in classical one.

I'm not a cosmologist, but AFAIU the Hilbert formalism of QM relies on Hilbert spaces always having a basis, which is famously equivalent to the Axiom of Choice. I'm not sure you can formulate the concept of self-adjoint operators without that, at least for arbitrary Hilbert spaces.

My suspicion is that AoC simply broadens the class of phase spaces to include pathological ones that "don't actually matter," so your point probably stands in all practical applications. However, it would take (hard) work to carefully extricate AoC from the current formalisms.

[_0w8t]

I got impression that intuitionistic mathematical analysis refers to original Boyer papers. Which is in modern terminology is constructive mathematical analysis plus an axiom of the choice sequence. Intuitionistic logic on the other hand is a classical logic without the law of excluded middle. This is what the constructive mathematics uses and which was also used by Boyer.

And yes, as in practice all physically measurable spaces are of finite dimensions, so using a formalism that works assuming AoC for arbitrary spaces is OK. The only danger is that one reads too much from it and assumes that the real world is like that.