Satz von Trachtenbrot

aus Wikipedia, der freien Enzyklopädie
Zur Navigation springen Zur Suche springen

Der Satz von Trachtenbrot, benannt nach Boris Trachtenbrot, ist ein Satz aus der mathematischen Logik. Er wurde 1950 bewiesen[1] und besagt, dass die in allen endlichen Modellen allgemeingültigen Sätze der Prädikatenlogik erster Stufe nicht rekursiv aufzählbar sind. Daraus ergeben sich Konsequenzen für die Prädikatenlogik zweiter Stufe.

Formulierungen des Satzes[Bearbeiten | Quelltext bearbeiten]

Es sei die Symbolmenge mit abzählbar unendlich vielen Konstantensymbolen und für jede Stelligkeit abzählbar unendlichen vielen Funktions- und Relationssymbolen. Weiter sei die Menge aller -Sätze der Prädikatenlogik erster Stufe, die in allen endlichen -Strukturen erfüllt sind. Dann gilt:

ist nicht rekursiv aufzählbar.

Kurzfassung: Die im Endlichen allgemeingültigen Sätze erster Stufe sind nicht rekursiv aufzählbar.[2]

Weiter sei die Menge aller -Sätze, zu denen es eine -Struktur gibt, in der sie erfüllt sind. Dann gilt:

ist nicht entscheidbar.

Kurzfassung: Die im Endlichen erfüllbaren Sätze erster Stufe sind nicht entscheidbar.[3][4]

Bemerkung zum Beweis[Bearbeiten | Quelltext bearbeiten]

Die zweite Formulierung wird auf die Unlösbarkeit des Halteproblems zurückgeführt, in dem man ausnutzt, das sich Turing-Maschinen in endlichen Modellen beschreiben lassen. Daraus ergibt sich dann die zuerst genannte Fassung, denn die im Endlichen allgemeingültigen Sätze sind genau die Negationen der im Endlichen nicht erfüllbaren Sätze.

Unvollständigkeit der Prädikatenlogik zweiter Stufe[Bearbeiten | Quelltext bearbeiten]

Als Anwendung zeigen wir, wie aus dem Satz von Trachtenbrot die Unvollständigkeit der Prädikatenlogik zweiter Stufe folgt. Es sei die Menge der Sätze der Prädikatenlogik zweiter Stufe, die in allen Modellen gültig sind. Dann gilt:

ist nicht rekursiv aufzählbar.

Diesen Sachverhalt nennt man die Unvollständigkeit der Prädikatenlogik zweiter Stufe. Zum Beweis sei ein Satz der Prädikatenlogik zweiter Stufe, der genau in endlichen Modellen gilt, etwa

,

d. h. für alle gilt, wenn eine Funktion ist und injektiv ist, dann ist surjektiv. Wäre nun rekursiv aufzählbar, so starte man ein Aufzählungsverfahren und immer dann, wenn dieses eine Aussage der Form mit einem -Satz der Prädikatenlogik erster Stufe erzeugt, gebe man aus. Auf diese Weise werden alle im Endlichen allgemeingültigen Sätze erster Stufe aufgezählt, was dem Satz von Trachtenbrot widerspricht.[5]

Einzelnachweise[Bearbeiten | Quelltext bearbeiten]

  1. B. Trakhtenbrot: Die Unmöglichkeit eines Algorithmus für das Entscheidungsproblem im Endlichen (Russisch), Doklady Akademii Nauk SSSR (1950), Band 70, Seiten 569–572. Englische Übersetzung in American Mathematical Society, Translations (1963), Series 2, Band 23, Seiten 1–5.
  2. H.-D. Ebbinghaus, J. Flum, W. Thomas: Einführung in die mathematische Logik, Spektrum Akademischer Verlag, ISBN 3-8274-0130-5, X, Satz 5.4
  3. H.-D. Ebbinghaus, J. Flum, W. Thomas: Einführung in die mathematische Logik, Spektrum Akademischer Verlag, ISBN 3-8274-0130-5, X, Satz 5.3
  4. H.-D. Ebbinghaus, J. Flum, W. Thomas: Finite Model Theory, Springer Verlag, ISBN 3-540-28787-6, Theorem 7.2.1
  5. H.-D. Ebbinghaus, J. Flum, W. Thomas: Einführung in die mathematische Logik, Spektrum Akademischer Verlag, ISBN 3-8274-0130-5, X, Satz 5.5