On: Kurt Gödel and the Mechanization of Mathematics

[Scarblac]

The law of the excluded middle says that for all propositions, either it or its negation must be true.

But Godel showed that there exist propositions for which neither can be proven.

[ProfHewitt → Scarblac]

The Law of Excluded Middle says:

   ⊢(Ψ or ~Ψ)

In inferential incompleteness says that there is a proposition Ψ such that:

  (⊬Ψ) and (⊬~Ψ)