Unentscheidbarkeit

(Alonzo Church 1938, Alan Turing 1937)

Das folgende Problem ist nicht entscheidbar:

• Eingabe: eine PL-Formel F mathend000#
• Ausgabe: Ja, gdw. F mathend000# 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) = mathend000# der Inhalt von Zelle i mathend000# zur Zeit t mathend000#.

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