 Solution

Take $\square A={\mathrm{Pr}}_{PA}(┌A┐)$ for the standard formal proof predicate symbol and putUse as given the arithmetization of syntax in PA, the derivability conditions, and the diagonal lemma. The latter supplies the fixed point needed in (a), and the former conditions interpret its normal modal distribution, necessitation on theorems and axiom4. Thus the argument in (a) proves the internal Löb implication in PA. With $X=\perp$ it readsThe inner implication is the first-order consistency first-order sentence $\neg \square \perp$, so contraposition givesThis is the arithmetic statement of the second incompleteness theorem proved within PA: if PA is first-order consistent, there is no PA formal proof of its first-order consistency first-order sentence. The displayed implication is a PA theorem without assuming that PA proves its antecedent.

For the corresponding external consequence, if a first-order consistent PA proved ${\mathrm{Con}}_{PA}$, theoremhood would give a formal proof of its boxed assertion. The displayed theorem together with the supposed formal proof of first-order consistency gives its negation, contradicting first-order consistency. Hence an externally first-order consistent PA does not prove its own first-order consistency.