Unentscheidbarkeit

(Alonzo Church 1938, Alan Turing 1937)

Das folgende Problem ist nicht entscheidbar:

• Eingabe: eine PL-Formel F
• Ausgabe: Ja, gdw. F allgemeingültig ist.

Beweis: man kodiert das Halteproblem für ein universelles Berechnungsmodell als eine logische Formel.

Für Turingmaschinen braucht man dafür „nur`` eine zweistellige Funktion

f (i, t) = der Inhalt von Zelle i zur Zeit t.

Beachte: durch diese mathematische Fragestellung (von David Hilbert, 1928) wurde die Wissenschaft der Informatik begründet.