= Solution
Write $BA=\exists y\,\operatorname{Prov}(\ulcorner A\urcorner,y)$ and fix a refutable <first-order sentence> $\bot$, so $S\vdash\neg\bot$ and $\operatorname{Con}_S=\neg B\bot$. First prove the internal equivalence
$$
\boxed{S\vdash G\leftrightarrow\operatorname{Con}_S.}
$$
Because $\bot\to G$ is provable, the <derivability conditions> give $B\bot\to BG$. The fixed-point equivalence $G\leftrightarrow\neg BG$ therefore yields $G\to\neg B\bot$.
For the reverse implication, necessitating $G\to\neg BG$ and applying distribution gives $BG\to B(\neg BG)$. <positive introspection> gives $BG\to B(BG)$. Finally the provable implication $BG\to(\neg BG\to\bot)$, necessitated and distributed, gives
$$
B(BG)\to\bigl(B(\neg BG)\to B\bot\bigr).
$$
Consequently $S\vdash BG\to B\bot$, so $\neg B\bot\to\neg BG\to G$. The same argument works with any chosen refutable <first-order sentence> in place of $\bot$; their formal consistency statements are provably equivalent.
By the classical <deduction theorem for propositional logic> applied to adjoining a <first-order sentence>, $S+\{G\}$ is consistent exactly when $S\nvdash\neg G$. The displayed equivalence makes $S+\{G\}$ and $S+\{\operatorname{Con}_S\}$ deductively equivalent. Therefore
$$
\boxed{S\nvdash\neg G\iff S+\{\operatorname{Con}_S\}\text{ is consistent}.}
$$
No soundness assumption on that extension is being substituted for consistency.
Back to article page
