Satz von Fagin

Der Satz von Fagin ist ein 1973 von Ronald Fagin bewiesener Satz aus der deskriptiven Komplexitätstheorie, der aussagt, dass die Menge aller mit Hilfe der existentiellen Prädikatenlogik zweiter Stufe beschreibbaren Sätze genau die Komplexitätsklasse NP ist.

Die existentielle Prädikatenlogik zweiter Stufe enthält Sätze, bei denen über die Prädikate eines Satzes aus der Prädikatenlogik erster Stufe existenzquantifiziert wird. Genauer handelt es sich um Sätze der Form

$\exists X_{1}\ldots \exists X_{k}\,\varphi (x_{1},\ldots ,x_{m},X_{1},\ldots ,X_{k})$

wobei der Ausdruck $\varphi (x_{1},\ldots ,x_{m},X_{1},\ldots ,X_{k})$ nur Quantifizierungen über die Individuenvariablen $x_{1},\ldots ,x_{m}$ aber keine Quantifizierungen über die Prädikatvariablen $X_{1},\ldots ,X_{k}$ enthält. Die Klasse NP ist die Klasse derjenigen Entscheidungsprobleme, die von einer nichtdeterministischen Turingmaschine in Polynomialzeit entschieden werden können. Das Bemerkenswerte an diesem Satz ist, dass er eine Komplexitätsklasse nur auf der Basis einer Logik charakterisiert, ohne dabei auf ein Berechnungsmodell wie Turingmaschinen zurückzugreifen. Damit begründete er die deskriptive Komplexitätstheorie.

Larry J. Stockmeyer verallgemeinerte das Ergebnis und zeigte, dass die Polynomialzeithierarchie durch die allgemeine Prädikatenlogik zweiter Stufe (mit Allquantoren) beschrieben wird.

Literatur

• R. Fagin. Generalized First-Order Spectra and Polynomial-Time Recognizable Sets (PDF; 2,0 MB). Complexity of Computation, ed. R. Karp, SIAM-AMS Proceedings 7, pp. 27–41. 1974.
• Neil Immerman: Descriptive Complexity. Springer, 1999, ISBN 0-387-98600-6, S. 113–119. 
• Heinz-Dieter Ebbinghaus, Jörg Flum: Finite Model Theory. Springer, 1999, ISBN 3-540-28787-6, S. 119–164.