Comment by andriy_koval
11 hours 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.
11 hours 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.
why should they be obvious? they are derived and have been thoroughly proven.
looks like we are in disagreement
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
6 replies →
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...
1 reply →