= Solution
For <unrestricted consistency self-strengthening is inconsistent>, again take $A=S+\neg\operatorname{Con}_S$. In $S^{++}$ the <axiom> $\operatorname{Con}_S$ and the preceding implication prove $\operatorname{Con}_A$. The additional rule then proves $\operatorname{Con}_{A+\operatorname{Con}_A}$.
However <consistent first-order theory>[consistency] of an extension implies <consistent first-order theory>[consistency] of its subtheory by the <monotonicity of inconsistency>[formalized inclusion of proofs]: $S\vdash\operatorname{Con}_A\to\operatorname{Con}_S$. Thus the ordinary <first-order theory>[theory] $A+\operatorname{Con}_A$ contains $\neg\operatorname{Con}_S$ and derives $\operatorname{Con}_S$, so it has a finite <contradiction> proof. Checking that concrete proof in arithmetic gives $S\vdash\neg\operatorname{Con}_{A+\operatorname{Con}_A}$. This theorem is also present in $S^{++}$, contradicting the result of the new rule. Therefore \b[$S^{++}$ is <consistent first-order theory>[inconsistent]].
The error in the added rule is its unrestricted internal use on arbitrary arithmetically presented systems, including systems containing false <consistent first-order theory>[consistency] assertions. A true external <consistent first-order theory>[consistency] progression for a specified sound system is not this unrestricted <inference rule>.
Back to article page
