Comment by thrance
1 year ago
The selection of which axioms to use is an interesting topic. Historically, axioms were first used by Hilbert and cie. while trying to progress in set theory. The complexity of the topic naturally led them to formalize their work, and thus arose ZF(C) [1], which later stuck as the de facto basis of modern mathematics.
Later systems, like Univalent Fundations [2] came from some limitations of ZFC and the desire to have a set of axioms that is easier to work with (for e.g. computer proof assistants). The choice of any new systems of axioms is ultimately limited by the scope of what ZFC can do, so as to preserve the past two centuries of mathematical works.
[1] https://en.wikipedia.org/wiki/Zermelo-Fraenkel_set_theory
Homotopy type theory (HoTT) > HoTT in CoQ: Coq-HoTT: https://github.com/leanprover/lean2/tree/master/hott
Lean4:
"Theorem Proving in Lean 4" https://lean-lang.org/theorem_proving_in_lean4/
Learnxinimutes > Lean 4: https://learnxinyminutes.com/lean4/
/? Hott in lean4 https://www.google.com/search?q=hott+in+lean4
> What is the relation between Coq-HoTT & Homotopy Type Theory and Set Theory with e.g. ZFC?
Then you add in the Brouwer Hilbert mess that still causes challenges with talking about where the a priori assumption of the law of the excluded middle causes real problems with modern computational challenge.
https://en.m.wikipedia.org/wiki/Brouwer%E2%80%93Hilbert_cont...
I think using the words 'fragment of' is less likely to cause issues than invoking constructivist mathematics.
But if anyone has better ideas how to explain what you lose with negation as failure etc... I am all ears.
Most of the popular ML methods require an assumption of IID, and C in ZFC both introduce LEM, which can be problematic for lots of people's ambitions.
It is difficult to not hit very passionate beliefs.