Zusammenfassung
Das Theorem von Church besagt, daß es kein effektives Verfahren gibt, um zu entscheiden, ob eine vorgegebene Formel ein Theorem der Quantifikationstheorie (Prädikatenlogik der ersten Stufe) ist, oder was damit äquivalent ist : ob diese Formel im quantifikatorischen (prädikatenlogischen) Sinn gültig ist35. Da die Quantifikationstheorie zur Logik im engeren Sinne gehört und die Existenz eines effektiven Verfahrens zur Lösung von bestimmten Problemen äquivalent ist mit der Existenz maschineller Lösungsmethoden für jene Probleme, kann man dieses Resultat auch etwas handgreiflicher so ausdrücken: Es ist unmöglich, eine Maschine zu erbauen, die für eine beliebige vorgelegte Aussage auf die Frage, ob diese Aussage rein logisch gültig sei, entweder „ja“ oder „nein“ zur Antwort gibt. Das „unmöglich“ ist hier nicht im Sinn von „faktisch unmöglich“, z. B. „physikalisch unmöglich“, zu verstehen, sondern im Sinn von „logisch unmöglich“ : die Annahme, eine derartige Maschine könnte konstruiert werden, führt zu einem logischen Widerspruch.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Literatur
Diese Äquivalenz beruht auf dem Vollständigkeitsbeweis für die Prädikatenlogik der ersten Stufe von GÖDEL [7], wonach alle gültigen Formeln der Quantifikationstheorie beweisbar sind. Vgl. auch HILBERT -ACKER -MANN [11], KLEENE [16] oder A. CHURCH [4]. Von nun an werden wir gelegentlich von semantischen Begriffen, wie „gültig“, „erfüllbar” usw., Gebrauch machen. Für das Verständnis der weiteren Ausführungen sind die intuitiven Erläuterungen, die wir für diese Begriffe geben, ausreichend. Es möge jedoch darauf hingewiesen werden, daß alle diese Begriffe mit Hilfe der von TARSxa entwickelten Methoden präzisiert werden können.
Für n = 0 geht die Prädikatvariable in eine Aussagenvariable über.
Durch diese Bestimmung sind insbesondere alle prim. rek. Funktionen eo ipso allg. rek.
Die „x; “ wurden hier der Einfachheit halber weggelassen.
Analoges gilt für den Fall, wo die Frage beantwortet werden soll, ob über das Bestehen oder Nichtbestehen einer Relation R zwischen solchen Objekten eine effektive Entscheidung herbeigeführt
Die unendlich vielen Individuenvariablen können durch die beiden Symbole „x“ und „$*”
Quantifikationsformel“ verwenden wir als sprachliche Abkürzung für „Formel der allgemeinen Quantifikationstheorie”.
tberflüssige Axiome werden dabei in der Weise ausgeschaltet, daß aus einer Klasse von Axiomen, welche nur durch Umbenennung der Individuen-variablen „x“, „y“, . auseinander hervorgehen, immer bloß ein einziges Axiom verwendet wird.
Das heißt (F) ist eine definitorische Abkürzung für jene primitive Formel (F’), die aus (F) durch ein-oder mehrmalige Anwendung des in D5 beschriebenen Verfahrens hervorgeht.
Man beachte, daß zu Beginn von Abschn. 7 als Interpretationen von Funktionszeichen solche Funktionen festgelegt worden sind, die Funktionswerte aus dem Individuenbereich nehmen, aus dem die Argumentwerte stammen. Dann sind alle Interpretationen von Ql und Q2 wahr.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 1959 Springer-Verlag Wien
About this chapter
Cite this chapter
Stegmüller, W. (1959). Die Unentscheidbarkeit der Quantifikationstheorie (Theorem von Church). In: Unvollständigkeit und Unentscheidbarkeit. Springer, Vienna. https://doi.org/10.1007/978-3-7091-3524-2_4
Download citation
DOI: https://doi.org/10.1007/978-3-7091-3524-2_4
Publisher Name: Springer, Vienna
Print ISBN: 978-3-7091-3525-9
Online ISBN: 978-3-7091-3524-2
eBook Packages: Springer Book Archive