Comment by czbot
8 months ago
ZFC allows models of second order PA and proves that those models are all isomorphic. Within each model of ZFC there is no such thing as a nonstandard model of second order PA. One can only think it is nonstandard by looking from outside the model, no? What theorem of second order PA is ZFC unable to prove?
This is similar to how there are countable models of ZFC but those models think of themselves as uncountable. They are countable externally and not internally.
The consistency of ZFC is (presumably) a theorem of second order PA, and ZFC is unable to prove it (unless ZFC is inconsistent).
Indeed yes. But in a sense within ZFC one can say what N is given the categorical nature of second order PA. Each model of ZFC will have, up to isomorphism, one model of N.