= Solution
The <Hilbert-Bernays-Löb derivability conditions> are: if $S\vdash A$ then $S\vdash\Box A$; $S\vdash\Box(A\to B)\to(\Box A\to\Box B)$; and $S\vdash\Box A\to\Box\Box A$. The first is an external rule about provability; the latter two are internal theorems. Standard numerical correctness and the stipulated $\Sigma_1$ form accompany the predicate in this question. These conditions do not include <full local reflection in a one-sentence extension is inconsistent>[reflection] $\Box A\to A$.
Choose a fixed refutable sentence $\bot$ and identify $\operatorname{Con}_S$ with $\neg\Box\bot$. Different fixed refutable choices have provably equivalent <consistent first-order theory>[consistency] sentences, because $S$ proves their equivalence to a <contradiction>. From $\bot\to G$, <necessitation rule>[necessitation] and <normal modal distribution axiom>[distribution] give $\Box\bot\to\Box G$. Since $G\to\neg\Box G$, this yields $G\to\operatorname{Con}_S$.
For the converse, necessitate $G\to\neg\Box G$ and distribute to get $\Box G\to\Box\neg\Box G$. <Positive introspection> also gives $\Box G\to\Box\Box G$. The two boxed contradictories imply $\Box\bot$ by formalized <classical propositional logic>[propositional reasoning]. Thus $\Box G\to\Box\bot$, and contraposition gives $\operatorname{Con}_S\to\neg\Box G\to G$. Consequently
$$
\boxed{S\vdash G\leftrightarrow\operatorname{Con}_S.}
$$
Finally the <deduction theorem for first-order logic>[deduction theorem] says that $S+G$ is <consistent first-order theory>[inconsistent] exactly when $S\vdash\neg G$. The internal equivalence identifies $S+G$ and $S+\operatorname{Con}_S$ in their deductive consequences. Hence \b[$S\nvdash\neg G$ exactly when $S+\operatorname{Con}_S$ is <consistent first-order theory>[consistent]]. <consistent first-order theory>[Consistency] of $S$ alone need not ensure this stronger <consistent first-order theory>[consistency] condition.
Back to article page
