6 ms·
There is, or rather are, fully recognized axiomatic foundations. You are free to choose one you like. Of the most popular ones is ZFC or ZF, but there are other
by deepsun 13d ago
There is, or rather are, fully recognized axiomatic foundations. You are free to choose one you like. Of the most popular ones is ZFC or ZF, but there are others (some lead to the same results some not). The main criteria for popularity is how useful it is. You can even make your own axiomatic where 2+2=5, but it would be useless.
You probably heard about Goedel Incompleteness -- the proof that the the axiomatic itself cannot be proven, like using ZFC to prove ZFC, but that's another topic.
It would be fun to play with this Anthropic/Lean formalization under different axiomatics.
- andriy_koval 13d ago> Goedel Incompleteness -- the proof that the the axiomatic itself cannot be proven, like using ZFC to prove ZFC, but that's another topic. Godel theorems are for systems with basic arithmetic, zfc doesn't include arithmetic, thus are not object of Godel theorems.
- Almondsetat 13d agoIf you start with "I'm not a strong expert" maybe you should stop continuing saying wrong stuff. What you just wrote is completely wrong.
- andriy_koval 13d agosupport your point with explanation or be ignored :-)
- Almondsetat 13d agoGodel proved that any system expressive enough to produce an arithmetic is incomplete. He initially proved it for the peano axioms but then it got generalized. ZFC can produce an arithmetic. Also, before being arrogant and demanding explanations, you should give them first for your claims
- andriy_koval 13d ago> expressive enough to produce you understand that "expressive enough to produce" are not obvious elements of zfc, that's some average consumer napkin math and not strict formalization.
- Almondsetat 13d agowhy should they be obvious? they are derived and have been thoroughly proven.
- andriy_koval 13d agolooks like we are in disagreement
- Almondsetat 13d agoA quick google search shows different proof assistants have been used to obtain the Peano axioms from ZFC, such as Isabelle/ZF and Metamath. I think you're just wrong
- cdelsolar 12d agoWhat are you nerds fighting about please explain
- deleted 12d ago[deleted]
- andriy_koval 13d agoyou are entitled to have your opinion :-)
- Almondsetat 13d agoand you are entitled to talk about maths while rejecting maths
- IsTom 13d ago> Moreover, Robinson arithmetic can be interpreted in general set theory, a small fragment of ZFC. https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory#Consistency https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t...
- andriy_koval 13d ago> interpreted its hard to me to tell what this means formally(as I said I am not expert). There is no "interpret" operator in zfc. I believe what it says if you add some robinson axioms + some logical rules on top of zfc, you can carry your results.
- IsTom 12d agoIt's the same way you don't need to have GCD in stdlib to say that you can compute GCD in C++. You can make your own using parts given. You don't need to add any axioms, you just build some sets to represent numbers and make operations that act the same way as arithmetic, define some equality relations. Then you derive rules of arithmetic for your handcrafted arithmetic using ZF axioms and you're good. You get axioms of arithmetic derived from your regular axioms without adding them as new axioms to your theory.
- andriy_koval 12d ago> you just build some sets to represent numbers and make operations that act the same way as arithmetic which is already "just" some non trivial problem(there is no "operations" in set theory), and we are discussing if it is achievable.
- IsTom 12d agoYou make relations and functions out of sets and prove theorems about them, reducing definition of things in terms of belonging to a set. This isn't particularly complicated.
- 12d ago
- jibal 13d agoThat is wildly wrong.
- drdeca 12d agoZFC has greater consistency strength than PA. If we take ZFC (or some other set theory) as our meta theory, we can easily see that the axiom of infinity (of ZFC) gives a set of natural numbers (using the von Neumann encoding), which, when equipped with the successor function, is a model of the natural numbers.
- andriy_koval 12d agozfc doesn't have functions, so you are building something new on top of it. Also, I am not sure successor function is enough for PA.
- Smaug123 12d agoIt simply does have functions. According to ZFC, a function is a set whose members are pairs, such that no two different pairs have the same first element. I mean this quite seriously: have you considered reading any first course in set theory?
- andriy_koval 12d ago> According to ZFC, a function is a set whose members are pairs, such that no two different pairs have the same first element. Can you cite where did you get this?
- Smaug123 12d agoAs I have said a few times now, you should read any first course in set theory. I’m quoting my third-year notes from Cambridge there, but essentially every intro to set theory will say the same. (I’m sure someone will find a single counterexample that does it somehow differently.)
- andriy_koval 12d agoYour third year notes from Cambridge has very low authority to me
- SP3269 13d agoInterestingly, in his ICM 2026 lecture, Terence Tao specifically mentioned that Lean is not based on ZFC.
- deterministic 12d agoLean is based on Type Theory not ZFC.
- deepsun 11d agoI always wanted to, say, look at any theorem and see what axiomatic it requires. Or in other way, see the theorem tree like in the article under a different set of axioms. Of course, for some results there are proofs discovered only under one axiomatic, but it's true under some others as well, just the proof wasn't discovered yet.