Basing the development of foundations on existence of a monster can lead to serious errors. For example, the [Gödel 1931] conclusion that a theory that axiomatizes is own provability cannot prove its own consistency was based on existence of the proposition I’mUnprovable (such that I’mUnprovable ⇔⊬I’mUnprovable). However, the [Gödel 1931] construction of I’mUnprovable fails in foundations because it violates restrictions on orders for propositions.
Nonexistence of Gödel’s proposition I’mUnprovable opened up the question of a theory being able to prove its own consistency. [Gödel 1931] included provability axioms for Russell’s system including the following:
· ModusPonens: ⊢(Φ⋀(Φ⇒Ψ)⊢Ψ)
Although not included in [Gödel 1931], the incorporations of TheoremUse {⊢( (⊢Ψ)⇒Ψ)} is fundamental to foundational theories by enabling the principle that theorems can be used in subsequent proofs. As such, TheoremUse belonged in the [Gödel 1931] axiomatization of provability for Russell’s Principia Mathematica. However, its inclusion would have made [Gödel 1931] inconsistent. Not including TheoremUse made the [Gödel 1931] axiomatization of provability fundamentally incomplete.
Inconsistency of a theory (¬Consistent) can be formally defined as there being a proposition Ψ0 such that ⊢Ψ0∧¬Ψ0.
Contra [Gödel 1931], a foundational theory can prove its own consistency as shown in the following theorem:
Theorem. ⊢Consistent
Proof. In order to obtain a contraction, hypothesize ¬Consistent. Consequently, there is a proposition Ψ0 such that ⊢Ψ0∧¬Ψ0. By the principle of TheoremUse
{((⊢Φ)⇒Φ)} with Ψ0 for Φ, Ψ0∧¬Ψ0, which is the desired contradiction.
However, the proof does not carry conviction that a contradiction cannot be derived because the proof is valid even if the theory is inconsistent. Consistency of the mathematical theories Actors and Ordinals is established by proving each theory has a unique-up-to-isomorphism model with a unique isomorphism.
See the following for more information:
"Epistemology Cyberattacks"
https://papers.ssrn.com/abstract=3603021