Comment by btilly

Are they?

The idea that uncountable means more comes from a bad metaphor. See https://news.ycombinator.com/item?id=44271589 for my explanation of that.

Accepting that uncountable means more forces us to debatable notions of existence. See https://news.ycombinator.com/item?id=44270383 for a debate over it.

But, finally, there is this. Every chain of reasoning that we can ever come up with, can be represented on a computer. So even if you wish to believe in some extension of ZFC with extremely large sets, PA is capable of proving every possible conclusion from your chosen set of axioms. So yes, PA is enough.

If you're not convinced, I recommend reading https://www.amazon.com/G%C3%B6del-Escher-Bach-Eternal-Golden....