[Gödel 1931] proposed the proposition I’mUnprovable (such that I’mUnprovable ⇔⊬I’mUnprovable) for proving inferential undecidability of Russel’s foundational

[Gödel 1931] proposed the proposition I’mUnprovable (such that I’mUnprovable ⇔⊬I’mUnprovable) for proving inferential undecidability of Russel’s foundational theory, which had the type-restriction on orders of propositions to prevent inconsistencies. I’mUnprovable cannot be constructed in foundational theories because strong types prevent construction of I’mUnprovable using the following recursive definition (see Diagonal Lemma [Gödel 1931]): I’mUnprovable:Proposition<i>≡⊬I’mUnprovable. Note that (⊬I’mUnprovable):Proposition<i+1> in the right-hand side of the definition because I’mUnprovable:Proposition<i> is a propositional variable in the definition ⊬I’mUnprovable. Consequently, I’mUnprovable:Proposition<i>⇒I’mUnprovable:Proposition<i+1>, which is a contradiction.