Die Unentscheidbarkeit der Quantifikationstheorie (Theorem von Church)

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.