Solution (source code)

= Solution

By part (c), <one-consistency> gives <Sigma-1 soundness> and hence ordinary consistency. First, $S$ cannot prove $\neg G$: if it did, the diagonal equivalence would give $S\vdash\Box G$. This is a $\Sigma_1$ sentence, so soundness would make it true. The stipulated standard interpretation of the <arithmetical provability predicate> would then supply an actual proof of $G$, contradicting consistency.

Now suppose $S\vdash\Box\neg G$. This too is a $\Sigma_1$ theorem. Soundness and the standard correctness of the predicate would imply that there is an actual $S$-proof of $\neg G$, which was just excluded. Therefore
$$
\boxed{S\text{ one-consistent}\ \Longrightarrow\ S\nvdash\Box\neg G.}
$$
The two applications of soundness concern the provability assertions, not the truth of arbitrary <arithmetic> sentences.