[FOM] Gödel’s Incompleteness Theorems

[Ken Kubota]

Dear list members,

Please take note of the abstract attached below. The publication reveals a weakness in the mechanized proof of Gödel’s Incompleteness Theorems by Lawrence C. Paulson mentioned in this list (http://www.cs.nyu.edu/pipermail/fom/2015-April/018648.html). Details are available at:
	http://dx.doi.org/10.4444/100.102

Two announcements may be of interest, available online at the mailing list system of the University of Cambridge, and at Google Groups.

Extended version of Gödel’s First Incompleteness Theorem:
	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-July/msg00059.html
	https://groups.google.com/d/msg/fa.isabelle/u396X_vbaZg/Mc-MX8-Wt0oJ

Download links:
	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-July/msg00060.html
	https://groups.google.com/d/msg/fa.isabelle/Vxhkk5I99L0/THhVW1tPj98J

Kind regards,

Ken Kubota


Abstract
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 “⊢α –> ⊢β” or “⊢α <–> ⊢β” 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.