Parameters
Categories
More about the book
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.
Book purchase
Gödel revisited, Ken Kubota
- Language
- Released
- 2015
Payment methods
- Title
- Gödel revisited
- Language
- English
- Authors
- Ken Kubota
- Publisher
- Owl of Minerva Press
- Publisher
- 2015
- Format
- Paperback
- ISBN10
- 3943334066
- ISBN13
- 9783943334067
- Category
- Mathematics
- Description
- 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.