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
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.
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
What are you nerds fighting about please explain
1 reply →
you are entitled to have your opinion :-)
3 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...
imo, those two links are example of rather low quality weird math discussions, but you can keep your opinion