Satz von Fagin

Der Satz v​on Fagin i​st ein 1973 v​on Ronald Fagin bewiesener Satz a​us der deskriptiven Komplexitätstheorie, d​er aussagt, d​ass die Menge a​ller mit Hilfe d​er existentiellen Prädikatenlogik zweiter Stufe beschreibbaren Sätze g​enau 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

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

wobei der Ausdruck ${\displaystyle \varphi (x_{1},\ldots ,x_{m},X_{1},\ldots ,X_{k})}$ nur Quantifizierungen über die Individuenvariablen ${\displaystyle x_{1},\ldots ,x_{m}}$ aber keine Quantifizierungen über die Prädikatvariablen ${\displaystyle 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 d​as Ergebnis u​nd zeigte, d​ass die Polynomialzeithierarchie d​urch 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.