nach oben

Erschienen in:

2022 | OriginalPaper | Buchkapitel

8. Gödel’s First Incompleteness Theorem via the Halting Problem

verfasst von : George Tourlakis

Erschienen in: Computability

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

It is rather surprising that Unprovability and Uncomputability are intimately connected. Gödel’s original proof of his first incompleteness theorem did not use methods of computability —indeed computability theory was not yet developed.

Before we turn to an elementary proof of the incompleteness theorem that is based on the unsolvability of the halting problem —hence our opening remarks— we show here, in outline, how he did it in Gödel (Monatshefte für Math Phys 38:173–198, 1931).

He constructed a sentence (closed formula) D (“D” for diagonal, since diagonalisation was at play in Gödel’s proof.) in the language of Peano Arithmetic (PA) that meant —when interpreted in the standard model— “I am not a (PA) theorem”.

This idea was based on a variation —namely, “I am lying”— of the “liar’s paradox” of the ancient Cretan philosopher Epimenides. (His original version was “All Cretans are liars”).

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Yet Another Number-Theoretic Characterisation of

Nächstes Kapitel The Second Recursion Theorem

“D” for diagonal, since diagonalisation was at play in Gödel’s proof.

His original version was “All Cretans are liars”.

See Sect. 0.2.

We encountered and used m-adic notation in Chap. 7 in order to code sequences of numbers. A more thorough use of this notation will occur in Chap. 12.

The reader will agree by looking back to Sect. 0.2 that one can easily write a, say, C-program to check whether or not a string A over the alphabet (2) is a wff. That is, in the sense explained in Remark 5.3.2, and by Church’s thesis, the set of all wff is recursive.

A particularly famous choice of axioms is due to Peano —the resulting theory then being called Peano arithmetic, in short PA. It has axioms that define the behaviour of every mathematical symbol, plus includes the induction axiom schema:

$$\displaystyle \begin{aligned}P(0)\land(\forall x)(P(x)\to P(Sx))\to P(x)\end{aligned}$$

The schema (or form, in English) gives one axiom for each choice of wff P.

We can mechanically check if they are applicable, or if they were applied in a step of some proof.0

Also (Bourbaki 1966; Enderton 1972).

There is no “it depends” in Tourlakis (2008) as the concrete interpretation is always without free variables.

Minimal: Defined connectives are not included.

For something like “(” or “)” that we may be using to open or close a parenthetical statement, or are just talking about it, we sometimes employ quotes to make clear that it is the latter case.

“Bew” for Beweis=Proof.

The Arithmetical relations have a lot of tolerance for variations in the choice of “initial” relations in their definition: Sometimes as much as all of $\mathcal {R}_{*}$ is taken as the initial Arithmetical relations. Sometimes as little as z = x + y and z = x × y. For technical convenience here we have added the graph of exponentiation here rather than choosing the most minimalist approach.

Gödel proved all this without the need to have exponentiation as a primitive operation in arithmetic. However, adopting this operation makes things considerably easier and, as mentioned earlier (footnote 13 on p. 12), it does not change the set of Arithmetical relations.

Again recall that x ^y is that of Example 2.1.16, and $ x ^{y+1} \mathop {|} z\equiv (\exists u)( u= y+1 \land x ^{u} \mathop {|} z)$. On the other hand, $x ^{u} \mathop {|} z \equiv (\exists w)(w=x ^{u}\land w \mathop {|} z)$.

J. Bennett, On Spectra. Ph.D. Thesis, Princeton University, (1962)

N. Bourbaki, Éléments de Mathématique; Théorie des Ensembles (Hermann, Paris, 1966)MATH

H.B. Enderton, A Mathematical Introduction to Logic (Academic Press, New York, 1972)MATH

K. Gödel, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für Math. Phys. 38, 173–198 (1931) (Also in English in M. Davis, The Undecidable (Raven Press, Hewlett, 1965), pp. 5–38)

A. Grzegorczyk, Some classes of recursive functions. Rozprawy Matematyczne 4, 1–45 (1953)MathSciNetMATH

E. Mendelson, Introduction to Mathematical Logic, 3rd edn. (Wadsworth & Brooks, Monterey, 1987)

J.R. Shoenfield, Mathematical Logic (Addison-Wesley, Reading, 1967)MATH

R.M. Smullyan, Theory of Formal Systems. Number 47 in Annals of Math. Studies (Princeton University Press, Princeton, 1961)

G. Tourlakis, Lectures in Logic and Set Theory, Volume 1: Mathematical Logic (Cambridge University Press, Cambridge, 2003a)CrossRef

G. Tourlakis, Mathematical Logic (Wiley, Hoboken, 2008)CrossRef

Titel: Gödel’s First Incompleteness Theorem via the Halting Problem
verfasst von: George Tourlakis
Verlag: Springer International Publishing
Buch: Computability
Print ISBN: 978-3-030-83201-8

Electronic ISBN: 978-3-030-83202-5

Copyright-Jahr: 2022
DOI: https://doi.org/10.1007/978-3-030-83202-5_8

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"