[thrance]

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

[2] https://en.wikipedia.org/wiki/Univalent_foundations

[westurner]

Homotopy type theory (HoTT) https://en.wikipedia.org/wiki/Homotopy_type_theory

/? From a set like {0,1} to a wave function of reals in Hilbert space [to Constructor Theory and Quantum Counterfactuals] https://www.google.com/search?q=From+a+set+like+%7B0%2C1%7D+... , https://www.google.com/search?q=From+a+set+like+%7B0%2C1%7D+...

From "What do we mean by "the foundations of mathematics"?" (2023) https://news.ycombinator.com/item?id=38102096#38103520 :

> HoTT in CoQ: Coq-HoTT: https://github.com/HoTT/Coq-HoTT

>>> The HoTT library is a development of homotopy-theoretic ideas in the Coq proof assistant. It draws many ideas from Vladimir Voevodsky's Foundations library (which has since been incorporated into the UniMath library) and also cross-pollinates with the HoTT-Agda library. See also: HoTT in Lean2, Spectral Sequences in Lean2, and Cubical Agda.

leanprover/lean2 /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?

[nyrikki]

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.