Within ZFC one can prove that any two models of second order PA are isomorphic. ZFC proves that PA is consistent. ZFC is good enough to capture arithmetical truth.
https://jdh.hamkins.org/the-universal-algorithm-a-new-simple...
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.