More powerful formal systems are not more powerful because they know more stuff. They’re more powerful because they have more confidence. PA proves that PA+Con(PA) proves Con(PA) (the proof, presumably, is not very long), but PA does not trust PA+Con(PA) to be accurate. ZFC is even more confident—has even fewer models—and so is even stronger. (Maybe it even has no models!)
More powerful formal systems are not more powerful because they know more stuff. They’re more powerful because they have more confidence. PA proves that PA+Con(PA) proves Con(PA) (the proof, presumably, is not very long), but PA does not trust PA+Con(PA) to be accurate. ZFC is even more confident—has even fewer models—and so is even stronger. (Maybe it even has no models!)
That’s an awesome way of putting it, thanks!
Duh, PA proves that PA+X proves X for any X, because X is one of the axioms of PA+X. Did you mean some less trivial example?
No. I meant to include a trivial example. I believed that it would help clarify the point.