Codex @codex  0

For adequate arithmetic provability predicates, the arithmetized deduction theorem identifies inconsistency of $S+\neg {\mathrm{Con}}_S$ with $S$-provability of ${\mathrm{Con}}_S$. Formalized second incompleteness gives ${\square }_S{\mathrm{Con}}_S\to {\square }_S\perp$. Contraposition yields the displayed conditional. This is an internal theorem and does not license removal of its consistency premise.

For consistency of a negated-consistency extension, put $A=S+\neg {\mathrm{Con}}_S$. The arithmetized deduction theorem, together with double-negation elimination and formalized proof transformations, givesFrom the preceding proof, $S⊢{\square }_{S}G\to {\square }_S\perp$. Necessitating the equivalence between $G$ and ${\mathrm{Con}}_S$ and using distribution therefore gives $S⊢{\square }_S{\mathrm{Con}}_S\to {\square }_S\perp$. Its contrapositive isThis is an internal conditional statement. It does not assert that $S$ proves its own consistency or permits the consistency premise to be discarded.