@TimothyChow: I'm not confusing anything. I didn't say we have to stop at PA at all. Didn't I mention ATR? The point is, the real world seems to have something like a standard model of PA, and that is the reason we even invented PA in the first place. Your argument about being able to add true arithmetic sentences applies only if you can justify your additional axioms as true. It gets harder and harder to do so, and it's unclear if you can go much further than ATR. — user21820 9 hours ago