Why PA has no set-theoretical model
We can define the usual order relation `‘ in PA so that every instance of the Induction Axiom schema such as, say:
yields the PA theorem:
Now, if we interpret PA without relativisation in ZF in the sense indicated by Feferman  — i.e., numerals as finite ordinals, as , etc. — then (ii) always translates in ZF as a theorem:
However, (i) does not always translate similarly as a ZF-theorem (which is why PA and ZF can have no common model), since the following is not necessarily provable in ZF:
Example: Define as `‘.
We conclude that we cannot appeal unrestrictedly to set-theoretical reasoning when studying the foundational framework of PA.
Reason: The language of PA has no constant that interprets in any model of PA as an arithmetical set of all natural numbers, and so the order relation `‘ and the concept of `terminating finitely’ over the numerals of PA in any model of PA cannot be taken to correspond as logically equivalent to the order relation `‘ and the concept of `terminating finitely’ over the ordinals in any putative model of Ordinal Arithmetic.
Moreover, the preceding sections show that it is the Axiom Schema of Finite Induction of PA that does not allow us to bypass this constraint by introducing an `actual’ (or `completed’) infinity disguised as an arbitrary constant—usually denoted by or —into either the language or a model of PA.
The standard Gödelian representation of Goodstein’s Theorem is not provable in PA
One formalisation of Goodstein’s Theorem in PA would then be the assertion that PA proves .
However any such proof would yield an algorithm that, for any natural number , would provide evidence that holds for some natural number , where is the interpretation of under a sound interpretation of PA over .
Since it can be shown  that there can be no such algorithm, we conclude that this formalisation of Goodstein’s Theorem cannot be proven in PA even if every Goodstein sequence were to terminate finitely over .
Return to 1: Solomon Feferman. 1992. What rests on what: The proof-theoretic analysis of mathematics. Invited lecture, 15th International Wittgenstein Symposium: Philosophy of Mathematics, held in Kirchberg/Wechsel, Austria, 16-23 August 1992. http://math.stanford.edu/~feferman/papers/whatrests.pdf
Return to 2: Elliott Mendelson. 1964. Introduction to Mathematical Logic. Van Norstrand, Princeton, p.131, Proposition 3.23.
Return to 3: Theorem VII in Kurt Gödel. 1931. On formally undecidable propositions of Principia Mathematica and related systems I. Translated by Elliott Mendelson. In M. Davis (ed.). 1965. The Undecidable. Raven Press, New York., p.29.