Hilbert believed every proposition is either provable or disprovable every mathematical proposition is, that is, inferentially decidable {(⊢Ψ) ∨ (⊢¬Ψ)} [Hilbert 1930]. Others doubted inferential decidability held. It would mean that whether a proposition is a theorem could be algorithmically decided by enumerating theorems until the proposition occurs or its negation occurs [von Plato 2018].
[Gödel 1931] seemed to have proved undecidability using the proposition I'mUnprovable, such that ⊢(I’mUnprovable ⇔⊬I’mUnprovable).
However, existence of I’mUnprovable would enable the following cyberattack [cf. Wittgenstein 1937]:
Theorem: Existence of I’mUnprovable of leads to inconsistency in foundations.
Proof: Ever since Euclid, it has been a fundamental principle that a theorem can be used in a proof (the principle of TheoremUse), that is, {⊢((⊢Ψ)⇒Ψ)} [cf. Artemov and Fitting 2019]. However by [Gödel 1931],
⊢(¬I’mUnprovable ⇔⊢I’mUnprovable). Consequently,
⊢(¬I’mUnprovable ⇒I’mUnprovable) by TheoremUse.
- Therefore ⊢I’mUnprovable using ProofBySelfContradiction
{⊢((⊢(¬Ψ⊢Ψ)) ⇒ ⊢Ψ)} with Ψ being I’mUnprovable.
- Thus, I’mUnprovable using TheoremUse {⊢((⊢Ψ)⇒Ψ)} with Ψ being I’mUnprovable.
Consequently, ⊬I’mUnprovable using
⊢(I’mUnprovable ⇔⊬I’mUnprovable)
Having both ⊢I’mUnprovable and ⊬I’mUnprovable is a contradiction in foundations.
Strong types prevent construction of I’mUnprovable using the following recursive definition:
I’mUnprovable:Proposition viw≡⊬I’mUnprovable. Note that (⊬I’mUnprovable):Proposition vi+1w in the right-hand side of the definition because I’mUnprovable is a propositional variable of I’mUnprovable :Proposition viw. Consequently,
I’mUnprovable:Proposition<i>⇒I’mUnprovable:Proposition<i+1>, which is a contradiction.
The crucial issue with the proofs in [Gödel 1931] is that the Gödel number of a proposition does not capture its order. Because of orders of propositions, the Diagonal Lemma [Gödel 1931] fails to construct the proposition I’mUnprovable.
information see the following: