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.