= Unrestricted consistency self-strengthening is inconsistent
Consider extending $S+\operatorname{Con}_S$ by a rule sending every $\operatorname{Con}_A$ to $\operatorname{Con}_{A+\operatorname{Con}_A}$. Put $A=S+\neg\operatorname{Con}_S$. The initial <consistent first-order theory>[consistency] <axiom> proves $\operatorname{Con}_A$ by the negated-consistency extension theorem, so the rule proves $\operatorname{Con}_{A+\operatorname{Con}_A}$. But $\operatorname{Con}_A\to\operatorname{Con}_S$ is provable by inclusion of proofs, making $A+\operatorname{Con}_A$ <consistent first-order theory>[inconsistent]. Arithmetic verifies its finite <contradiction> proof. Thus the unrestricted rule proves both that <first-order theory>[theory]'s <consistent first-order theory>[consistency] and inconsistency. This differs from an externally justified progression along specified sound <first-order theory>[theories].
Back to article page
