Auch andere Begriffe der Komplexitätstheorie lassen sich in die Logik übertragen, insbesondere die der Reduktion und des vollständigen Problems.
Das vollständige Problem, das uns hier interessiert, ist
das Geographiespiel.
Geographiespiele werden auf Strukturen mit einer Kantenrelation gespielt.
Die Spielerinnen ziehen von einer Startposition aus einen Spielstein
abwechselnd entlang einer Kante. Wer nicht ziehen kann, hat verloren. Das Problem, zu
entscheiden, wer das Geographiespiel auf einer gegebenen Struktur
mit einer gegebenen Startstellung gewinnt,
ist vollständig für
PTIME bezüglich LOGSPACE-Reduktion [JS76].
Die entsprechende Aussage in der Logik ist, daß das
Geographiespiel auf geordneten Strukturen
vollständig für IFP bezüglich DTC-Reduktion
ist.
Sie läßt sich in doppelter Weise verschärfen: Das Geographiespiel
ist vollständig für IFP, sogar bezüglich quantorenfreier Reduktion
auf allen endlichen Strukturen, auch ohne Ordnungsrelation
[Dah87]
Ausgangspunkt der Arbeit war die Frage, wie ausdrucksstark
Fixpunktoperatoren der Form
$[FP{X\bar x}\exists \bar z\notin X\fhi(\bar x,\bar z)]$
mit quantorenfreiem $\fhi$ sind.
Diese stehen in engem Zusammenhang mit dem Geographiespiel.
Betrachtet man $\fhi(\bar x,\bar z)$ als Definition einer Kantenrelation, so charakterisiert dieser Operator die Gewinnstellungen im zugehörigen Geographiespiel, wenn der Fixpunkt existiert.
Könnte man sich darauf verlassen, daß er existiert, so wäre es dank der Vollständigkeit des Geographiespiels leicht zu beweisen, daß solche Operatoren so ausdrucksstark sind wie IFP. Leider ist dies nicht der Fall. Er existiert nur, wenn das zugehörige Spiel remisfrei ist, d.h. wenn es keine Stellungen gibt, in denen keine der beiden Parteien eine Gewinnstrategie hat. Es stellt sich also die Frage, ob man mit solchen Formeln $\fhi(\bar x,\bar z)$ auskommt, die remisfreie Spiele definieren. Anders formuliert: Sind die remisfreien Geographiespiele vollständig für IFP?
Die Theorie der remisfreien Spiele hat sich als fruchtbar erwiesen. Unser Programm ist folgendes: Zunächst wird ein ``Hauptsatz'' bewiesen, der in etwa sagt, daß die remisfreien Geographiespiele tatsächlich vollständig für IFP bezüglich quantorenfreier Reduktion sind. Dieser wird direkt bewiesen, also ohne Rückgriff auf Normalformen oder sonstige Sätze über Fixpunktlogiken. Aus dem Hauptsatz folgt recht einfach eine schöne Normalform für IFP, die gleichzeitig IFP=LFP beweist. Zum Schluß beantworten wir, sozusagen als Anwendung, die Ausgangsfrage in einer allgemeineren Form.