Unrestricted consistency self-strengthening is inconsistent

ID: unrestricted-consistency-self-strengthening-is-inconsistent

Consider extending by a rule sending every to . Put . The initial consistency axiom proves by the negated-consistency extension theorem, so the rule proves . But is provable by inclusion of proofs, making inconsistent. Arithmetic verifies its finite contradiction proof. Thus the unrestricted rule proves both that theory's consistency and inconsistency. This differs from an externally justified progression along specified sound theories.

New to topics? Read the docs here!