upvote
Interestingly, in his ICM 2026 lecture, Terence Tao specifically mentioned that Lean is not based on ZFC.
reply
> 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.

reply
If you start with "I'm not a strong expert" maybe you should stop continuing saying wrong stuff. What you just wrote is completely wrong.
reply
support your point with explanation or be ignored :-)
reply
Godel 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
reply
> 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.

reply
why should they be obvious? they are derived and have been thoroughly proven.
reply
looks like we are in disagreement
reply
A 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
reply
What are you nerds fighting about please explain
reply
deleted
reply
you are entitled to have your opinion :-)
reply
and you are entitled to talk about maths while rejecting maths
reply
coming back to your argument about peano being obtained from zfc, you obviously can't prove that it happened using purely zfc, and not some logical framework embedded into those proof assistants.

I said I am not expert, I am indeed not expert in zfc and godel theorems, but I am an expert (phd) in actual formalization theory. Formal theory is very simple concept: its alphabet, set of formulas on top of this alphabet, and function which translates one formula to another.

ZFC can't "obtain" peano, simply because it doesn't have say * operator defined. You need to do something on top of it. Additionally, zfc itself looks like loosely formalized say in wikipedia (and I am not sure if there is any strict formalization anywhere), we take it as common sense that it can utilize some simple logical rules (e.g. modus ponens), but what are exactly rules, which could be separate topic of research, this detail is skipped.

reply
That increases the likelihood that they are right.

> support your point with explanation or be ignored :-)

Anyone who says "Godel theorems are for systems with basic arithmetic, zfc doesn't include arithmetic, thus are not object of Godel theorems" and isn't joking warrants a permanent ignore.

https://math.stackexchange.com/questions/1366560/why-does-g%...

https://math.stackexchange.com/questions/1090437/how-to-prov...

reply
imo, those two links are example of rather low quality weird math discussions, but you can keep your opinion
reply
> 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_t...

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

reply
ZFC 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.

reply
zfc 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.

reply
That is wildly wrong.
reply
Lean is based on Type Theory not ZFC.
reply