= Solution
Again abbreviate provability by $\Box$. The <Gödel sentence> equivalence gives $S\vdash G\to\neg\Box G$. Internalizing this implication using the first two <Hilbert-Bernays-Löb derivability conditions> gives
$$
S\vdash\Box G\to\Box\neg\Box G.
$$
<Positive introspection> also gives $S\vdash\Box G\to\Box\Box G$. Internal <modus ponens rule> combines proofs of a sentence and its <negation> into a proof of a contradiction; a contradiction implies any sentence. Consequently
$$
S\vdash\Box G\to\Box\neg G.
$$
These are syntactic manipulations of provability, not an appeal to <soundness>. If $S\vdash\neg\Box\neg G$, taking the contrapositive of the last implication gives $S\vdash\neg\Box G$, and the diagonal equivalence gives $S\vdash G$. Part (a) rules that out for a consistent theory. Hence
$$
\boxed{S\nvdash\neg\Box\neg G\quad\text{when }S\text{ is consistent}.}
$$
Back to article page
