3 ms·

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. T

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 https://en.wikipedia.org/wiki/Zermelo-Fraenkel_set_theory [2] https://en.wikipedia.org/wiki/Univalent_foundations https://en.wikipedia.org/wiki/Univalent_foundations

nyrikki 2y ago
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_controversy 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.
westurner 2y ago
Homotopy type theory (HoTT) https://en.wikipedia.org/wiki/Homotopy_type_theory 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+to+a+wave+function+of+reals+in+Hilbert+space 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+to+a+wave+function+of+reals+in+Hilbert+space+%5Bto+Constructor+Theory+and+Quantum+Counterfactuals%5D+ 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 https://news.ycombinator.com/item?id=38102096#38103520 : > HoTT in CoQ: Coq-HoTT: https://github.com/HoTT/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 https://github.com/leanprover/lean2/tree/master/hott Lean4: "Theorem Proving in Lean 4" https://lean-lang.org/theorem_proving_in_lean4/ https://lean-lang.org/theorem_proving_in_lean4/ Learnxinimutes > Lean 4: https://learnxinyminutes.com/lean4/ https://learnxinyminutes.com/lean4/ /? Hott in lean4 https://www.google.com/search?q=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 2y ago

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_controversy 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.

westurner 2y ago

Homotopy type theory (HoTT) https://en.wikipedia.org/wiki/Homotopy_type_theory 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+to+a+wave+function+of+reals+in+Hilbert+space 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+to+a+wave+function+of+reals+in+Hilbert+space+%5Bto+Constructor+Theory+and+Quantum+Counterfactuals%5D+ 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 https://news.ycombinator.com/item?id=38102096#38103520 : > HoTT in CoQ: Coq-HoTT: https://github.com/HoTT/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 https://github.com/leanprover/lean2/tree/master/hott Lean4: "Theorem Proving in Lean 4" https://lean-lang.org/theorem_proving_in_lean4/ https://lean-lang.org/theorem_proving_in_lean4/ Learnxinimutes > Lean 4: https://learnxinyminutes.com/lean4/ https://learnxinyminutes.com/lean4/ /? Hott in lean4 https://www.google.com/search?q=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?