[ProfHewitt]

Russell's rules for orders on propositions rule out the existence of the [Gödel 1931] proposition I'mUnprovable (such that I'mUnprovable <=> ~⊢I'mUnprovable)

There is no fixed point (Diagonal Lemma) for the mapping Ψ↦~⊢Ψ because the order of the proposition ~⊢Ψ is one greater than the order of the proposition Ψ because Ψ is a propositional variable.

For a correct formal proof that there are true but unprovable propositions in the most powerful foundations see the following:

    Physical Indeterminacy in Digital Computation

https://papers.ssrn.com/abstract=3459566