= Solution
The definition of $a$ makes the diagonal instance $E_a[\bar a]$ exactly $G_S$. The representing <logical formula> therefore has the standard interpretation
$$
\mathbb N\models\exists v_2A(\bar a,v_2)\quad\Longleftrightarrow\quad S\vdash G_S.
$$
If $S\vdash G_S$, choose an actual witness $m$ to the left-hand existential statement. The <bounded arithmetic sentence> $A(\bar a,\bar m)$ is true and hence provable by $\Sigma_0$-completeness. But $G_S$ also gives $S\vdash\neg A(\bar a,\bar m)$, a <contradiction>. Thus
$$
\boxed{S\text{ consistent}\quad\Longrightarrow\quad S\nvdash G_S.}
$$
Now assume <one-consistency>. It implies <first-order consistency>, so no <formal proof> of $G_S$ exists and $A(a,m)$ is false for each standard $m$. Each <bounded arithmetic sentence> $\neg A(\bar a,\bar m)$ is consequently true and provable. A <formal proof> of $\neg G_S$ would give a <formal proof> of $\exists v_2A(\bar a,v_2)$ while every standard witness instance is refuted, contrary to <one-consistency>. Hence
$$
\boxed{S\text{ one-consistent}\quad\Longrightarrow\quad S\nvdash\neg G_S.}
$$
The two hypotheses play different roles: ordinary <first-order consistency> excludes the positive <Gödel sentence>, while the stronger hypothesis also excludes its <negation>.
Back to article page
