- ホーム
- > 洋書
- > ドイツ書
- > Mathematics, Sciences & Technology
- > Mathematics
- > basics
Description
(Text)
With 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, in the case of Paulson even machine-assisted. 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 occurences of the deduction symbol () in order to express the relationship between (the provability of) theorems rather than just 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 toprove Gödel's Incompleteness Theorem in an object logic, as it 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, but not in an object logic, it cannot be considered as a (relevant) mathematical theorem anymore and 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 like "I am not provable" has the two logical properties of a classical paradox, negativity (negation) and self-reference.
