= Solution
First establish the transfer of provability requested in the hint. The propositional theorem $X\to(\neg G\to X)$ and the <derivability conditions> give
$$
S\vdash\Box X\to\Box(\neg G\to X).
$$
The supplied arithmetized deduction equivalence identifies the right-hand provability assertion, within $S^*$, with $\Box^*X$. Hence
$$
S^*\vdash\Box X\to\Box^*X.
$$
Choose a fixed <contradiction> $\bot$ for $X$. Part (b) gives $S\vdash G\leftrightarrow\neg\Box\bot$, so adjoining $\neg G$ gives $S^*\vdash\Box\bot$. The transfer implication now gives $S^*\vdash\Box^*\bot$.
Apply (b) inside $S^*$ to its own <Gödel sentence>: it proves $G^*\leftrightarrow\neg\Box^*\bot$. The last provability assertion therefore entails
$$
\boxed{S^*\vdash\neg G^*.}
$$
Thus the extension proves the <negation> of its own <Gödel sentence> as well. When $S$ is <first-order consistent>, (c) says this phenomenon occurs in a <first-order consistent> extension; the extension asserts an internal <formal proof> of <contradiction> without there being an actual standard <formal proof> of <contradiction>.
Back to article page
