Orders on propositions were introduced by Bertrand Russell to prevent inconsistencies in foundations of mathematics. Strong types prevent construction of I’mU

Orders on propositions were introduced by Bertrand Russell to prevent inconsistencies in foundations of mathematics. Strong types prevent construction of I’mUnprovable using the following recursive definition: I’mUnprovable:Proposition<i>≡⊬I’mUnprovable Note that (⊬I’mUnprovable):Proposition<i+1> in the right- hand side of the definition because I’mUnprovable is a propositional variable in the right-hand side. 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.