= Solution
For <consistency of a negated-consistency extension>, put $A=S+\neg\operatorname{Con}_S$. The <arithmetized deduction theorem>, together with double-negation elimination and formalized proof transformations, gives
$$
S\vdash\Box_A\bot\leftrightarrow\Box_S\operatorname{Con}_S,
\qquad S\vdash\operatorname{Con}_A\leftrightarrow\neg\Box_S\operatorname{Con}_S.
$$
From the preceding proof, $S\vdash\Box_SG\to\Box_S\bot$. Necessitating the equivalence between $G$ and $\operatorname{Con}_S$ and using <normal modal distribution axiom>[distribution] therefore gives $S\vdash\Box_S\operatorname{Con}_S\to\Box_S\bot$. Its contrapositive is
$$
\boxed{S\vdash\operatorname{Con}_S\to\operatorname{Con}_{S+\neg\operatorname{Con}_S}.}
$$
This is an internal conditional statement. It does not assert that $S$ proves its own <consistent first-order theory>[consistency] or permits the <consistent first-order theory>[consistency] premise to be discarded.
Back to article page
