Gödel revisited

In the presentations by Peter B. Andrews and Lawrence C. Paulson, two very different attempts to prove Gödel’s Incompleteness Theorem with a high level of formalization are available – even machine-assisted in the case of Paulson. Andrews’ system Q0 is an object logic, whereas the natural deduction system underlying the presentation by Paulson is a meta-logic, i. e. it is possible to express theorems of the form “> a --> > b” or “> a == > b” with two or more occurrences of the deduction symbol (>) in order to express the relationship between (the provability of) theorems rather than just the theorems themselves. Paulson’s proof yields a twofold result with a positive and a negative side. It is possible to prove in the meta-logic (assuming the semantic approach and the correctness of the software) the formal statement that from the consistency of the theory under consideration follows the existence of an unprovable theorem; on the other hand, Paulson’s proof demonstrates that it is impossible to prove Gödel’s Incompleteness Theorem in an object logic, as was shown for the case of Andrews’ system Q0 in [Kubota, 2013], and any attempt immediately results in inconsistency. But if Gödel’s Incompleteness Theorem, unlike mathematics in general, can only be expressed in a meta-logic, not in an object logic, it can no longer be considered a (relevant) mathematical theorem and it is only the result of the limited expressiveness of meta-logics in which the inconsistency of the theory under consideration cannot be expressed, although the construction of a statement such as “I am not provable” contains the two logical properties of a classical paradox: negativity (negation) and self-reference.