Using Orders on propositions, the construction of Gödel’s proposition I'mUnprovable is blocked because the mapping Ψ↦⊬Ψ has no fixed point because ⊬Ψ has order one greater than the order of Ψ since Ψ is a propositional variable. Consequently, some other way had to be devised to prove inferential incompleteness without using Gödel’s proposition I'mUnprovable. A complication is that theorems of strongly-typed theories of the natural numbers and computation are not computationally enumerable because there are uncountable instances of the induction axiom in each theory. However, proof checking is computationally decidable :-) The complication can be overcome using special cases of induction axioms to prove inferential incompleteness of the theories. See the following:
https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3418003