| The hard part in the proof for Gödel's first incompleteness theorem is what would later become known as Carnap's diagonal lemma: https://en.wikipedia.org/wiki/Diagonal_lemma#Proof This proof consists of just 7 lines, but these 7 lines are considered to be fiendishly unreadable. The lemma itself says otherwise something very understandable and perfectly relatable: logicSentence <-> prop(%logicSentence) Meaning of the lemma: If prop(%s) is a predicate property of any logic sentence s, then there exists at least one true sentence for which this property is true and/or one false sentence for which it is false. The expression %logicSentence is the (numerical) description (encoded as a number) of the logicSentence. The remainder of Gödel's proof is just endless bureaucracy to establish completely precisely in/from what type of theory it occurs/can be derived. If you leave out the bureaucracy, Gödel's first incompleteness theorem follows almost trivially from the lemma: logicSentence <-> isNotProvable(%logicSentence) Hence, according to the expression above, there exists at least one false sentence that is not isNotProvable (and is therefore provable) [a] or at least one true sentence that isNotProvable [b]. Hence, the theory in which this situation occurs is inconsistent [a] or incomplete [b]. Now, the bureaucracy in Gödel's full proof actually does matter, because his theorem holds for the Peano and Robinson formalizations of arithmetic theory but not for the Skolem and Presburger ones. The reasons for that can only be found in the bureaucracy of Gödel's proof. |
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:
https://papers.ssrn.com/abstract=3459566