= Solution
Take $\Box A=\operatorname{Pr}_{PA}(\ulcorner A\urcorner)$ for the standard <formal proof> <predicate symbol> and put
$$
\operatorname{Con}_{PA}=\neg\Box\bot.
$$
Use 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=\bot$ it reads
$$
PA\vdash\Box(\Box\bot\to\bot)\to\Box\bot.
$$
The inner implication is the <first-order consistency> <first-order sentence> $\neg\Box\bot$, so contraposition gives
$$
\boxed{PA\vdash\operatorname{Con}_{PA}\to
\neg\operatorname{Pr}_{PA}(\ulcorner\operatorname{Con}_{PA}\urcorner).}
$$
This 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 $\operatorname{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>.
Back to article page
