= Solution
Use the preceding fixed point with $q=\bot$. If the chosen arithmetic interpretation sends $\bot$ to a PA-refutable sentence $Z$, it gives the arithmetic sentence
$$
C=(BZ\to Z),\qquad\operatorname{PA}\vdash C\leftrightarrow(BC\to Z).
$$
This follows from <Arithmetical soundness of GL>. Since <Peano arithmetic> proves $\neg Z$, the two implications are equivalent to negated provability:
$$
\operatorname{PA}\vdash C\leftrightarrow\neg BZ,\qquad\operatorname{PA}\vdash C\leftrightarrow\neg BC.
$$
Thus $C$ expresses the <formal consistency statement> for <Peano arithmetic> and is also a negative provability fixed point, like its <Gödel sentence> $G$.
Apply the supplied modal uniqueness formula to the context with a <modalized occurrence> $X(p)=(\Box p\to\bot)$, with two fresh variables interpreted as $G$ and $C$. A <modalized occurrence> means that each indicated variable occurrence lies inside a box. <Peano arithmetic> proves both arithmetic fixed-point equations. The first derivability condition boxes those equations, so the translated uniqueness formula gives
$$
\operatorname{PA}\vdash B(G\leftrightarrow C).
$$
One must not infer $G\leftrightarrow C$ by reflection. Instead, distribution and the provability of the two propositional projections give $\operatorname{PA}\vdash BG\leftrightarrow BC$. Negating and using the two fixed-point equations now yields
$$
\boxed{\operatorname{PA}\vdash G\leftrightarrow C\leftrightarrow\neg BZ=\operatorname{Con}(\operatorname{PA}).}
$$
This proves the <Equivalence of a Gödel sentence and a consistency statement> using the required modal soundness, fixed point and uniqueness results.
Back to article page
