= Consistency of a negated-consistency extension
{title2=$S\vdash\operatorname{Con}_S\to\operatorname{Con}_{S+\neg\operatorname{Con}_S}$}
For adequate arithmetic <arithmetical provability predicate>[provability predicates], the <arithmetized deduction theorem> identifies inconsistency of $S+\neg\operatorname{Con}_S$ with $S$-provability of $\operatorname{Con}_S$. Formalized second incompleteness gives $\Box_S\operatorname{Con}_S\to\Box_S\bot$. Contraposition yields the displayed conditional. This is an internal theorem and does not license removal of its <consistent first-order theory>[consistency] premise.
Back to article page
