Nelson was right, and therefore even PA revision needed.

In order to prove ¬Con(PA) we start from the proof ¬Con(ZFC)...

https://www.researchgate.net/publication/322592032_There_is_no_standard_model_of_ZFC

https://philarchive.org/rec/FOUTIN-4

In order to prove ¬Con(PA) directly from PA, PA doesn't power enough to prove own inconsistency.

Let us remind that accordingly to naive set theory, any definable collection is a set. Let R be the set of all sets that are not members of themselves. If R qualifies as a member of itself, it would contradict its own definition as a set containing all sets that are not members of themselves. On the other hand, if such a set is not a member of itself, it would qualify as a member of itself by the same definition. This contradiction is Russell’s paradox. In 1908, two ways of avoiding the paradox were proposed, Russell’s type theory and Zermelo set theory, the first constructed axiomatic set theory. Zermelo’s axioms went well beyond Frege’s axioms of extensionality and unlimited set abstraction, and evolved into the now-canonical Zermelo–Fraenkel set theory ZFC.

"But how do we know that ZFC is a consistent theory, free of contradictions? The short answer is that we don’t; it is a matter of faith (or of skepticism)"— E.Nelson wroted in his paper [1].

nice question.

Notice it is widely believed that if ZFC and ZFC_2 were inconsistent, that fact would have been uncovered by now !!!

It agree, but in any case in this paper Nelson dealing only with standard objects.

He seems to be saying only that: there is not standard model of PA, i.e.

~Con(PA+∃MPAst )

Now I go to proof that:

~Con(Z2+∃Mst Z2) where Z2 an formal system very similar to PA.

See for example: Set Theory and the Continuum Hypothesis (Dove… (Paperback) by Paul J. Cohen. section 6

https://www.amazon.com/Theory-Continuum-Hypothesis-Dover-Mathematics/dp/0486469212