Had a short discussion on constructive formalized math with some people at Stockholm University (including him) a while ago, and we were unsure about the basic motivation behind the MathComp library/repo being axiom free. Was/is it mostly (or fully) because of minimalism rather than, say, foundational worries or foundational commitments?

I can't speak for everybody, but "adding axioms" is not compositional, so if a library picks some, you constraint what its users can pick. Using no axioms gives a lot of freedom to the users of the library. For example you can prove a CS instance of a choiceType using an axiom, if you like.

So IMO it is a sound engineering choice.

Enrico, I agree with the sound engineering part, but surely there is some breaking point in terms avoiding axioms when math gets more "complicated" and classical? Do you see analysis being merged into math-comp repo or living on separately? Monorepo packaging maybe enough to separate?

I don't know their integration plans, but MC analysis is in some sense a leaf of MC. I'm talking of axioms at the *root*, like placing them in m-c-ssreflect, so "merging MC analysis in" would not invalidate my remark.

As I understand it, analysis is one math topics where the classic and constructive variants diverge not only in the "cost" of proofs, but also in the shape of statements. So it is probably a good point where you have to fix your ground. Moreover if you want to use the hierarchy of MC on your object of study (the "real" reals) then you are kind of forced to postulate axioms (which are well accepted in that field).

Again, this is just my opinion.

Last updated: Feb 09 2023 at 03:06 UTC