Satz von Gaifman

Der Satz v​on Gaifman i​st ein Satz a​us der mathematischen Logik. Er s​agt aus, d​ass alle Sätze d​er Prädikatenlogik erster Stufe i​n endlichen, relationalen Strukturen i​n einem gewissen Sinne n​ur lokale Aussagen treffen können. Der Satz g​eht auf Haim Gaifman zurück u​nd stammt a​us dem Jahre 1981.[1]

Einführung

Es sei ${\displaystyle L_{I}^{\sigma }}$ eine relationale Sprache der Prädikatenlogik erster Stufe. Dabei bedeutet relational, dass die Signatur ${\displaystyle \sigma }$ nur aus endlich vielen Relationssymbolen besteht. Modelle bzw. Strukturen dieser Sprache werden ${\displaystyle \sigma }$ -Strukturen genannt. Ein wichtiges Beispiel ist ${\displaystyle \sigma =\{R\}}$ , wobei ${\displaystyle R}$ ein zweistelliges Relationssymbol ist. Eine ${\displaystyle \{R\}}$ -Struktur ist dann eine Menge ${\displaystyle G}$ mit einer zweistelligen Relation ${\displaystyle R^{G}}$ auf ${\displaystyle G}$ als Interpretation von ${\displaystyle R}$ . Derartige Strukturen sind nichts anderes als Graphen, wobei ${\displaystyle R^{G}(a,b)}$ bedeutet, dass die Knoten ${\displaystyle a,b\in G}$ durch eine Kante verbunden sind.

Die Idee, in Graphen kürzeste Wege zwischen Knoten als Abstände zu verwenden, überträgt man auf allgemeine endliche ${\displaystyle \sigma }$ -Strukturen ${\displaystyle {\mathfrak {A}}=(A,I)}$ mit Universum ${\displaystyle A}$ und Interpretation ${\displaystyle I}$ , indem man zum sogenannten Gaifman-Graphen ${\displaystyle G({\mathfrak {A}})}$ übergeht. Dieser Graph hat die Knotenmenge ${\displaystyle A}$ und zwei verschiedene Knoten ${\displaystyle a,b\in A}$ sind genau dann durch eine Kante verbunden, wenn es eine Relation ${\displaystyle R\in \sigma }$ mit Stelligkeit ${\displaystyle s(R)}$ und Elemente ${\displaystyle a_{1},\ldots ,a_{s(R)}\in A}$ mit ${\displaystyle R^{\mathfrak {A}}(a_{1},\ldots ,a_{s(R)})}$ und ${\displaystyle a,b\in \{a_{1},\ldots ,a_{s(R)}\}}$ gibt, wobei ${\displaystyle R^{\mathfrak {A}}}$ die Interpretation von ${\displaystyle R}$ unter ${\displaystyle I}$ ist. Kurz, ${\displaystyle a,b\in A}$ sind durch eine Kante verbunden, wenn sie in einer Relation zueinander stehen. Der Abstand ${\displaystyle d(a,b)}$ ist dann die Länge eines kürzesten Weges von ${\displaystyle a}$ nach ${\displaystyle b}$ im Gaifman-Graphen. Mittels dieses Abstandes kann man dann für ${\displaystyle {\vec {a}}:=(a_{1},\ldots ,a_{n})\in A^{n}}$ und ${\displaystyle r\in \mathbb {N} _{0}}$ wie folgt die r-Kugel um ${\displaystyle {\vec {a}}}$ definieren:

${\displaystyle B_{r}^{\mathfrak {A}}({\vec {a}}):=\{a\in A|\,\min _{i=1,\ldots ,n}d(a_{i},a)\leq r\}=\bigcup _{i=1}^{n}\{a\in A|\,d(a_{i},a)\leq r\}\subset A}$ .

Beachte dazu, dass weder der Abstand ${\displaystyle d}$ , noch der Vergleich ${\displaystyle \leq }$ , noch die natürliche Zahl r Bestandteil von ${\displaystyle L_{I}^{\sigma }}$ sind. Dennoch kann man in ${\displaystyle L_{I}^{\sigma }}$ über den Abstand und die r-Kugeln sprechen. Genauer gibt es ${\displaystyle \sigma }$ -Formeln ${\displaystyle \delta _{r}(x,y)}$ mit

${\displaystyle d(a,b)\leq r\quad \iff \quad {\mathfrak {A}}\vDash \delta _{r}(a,b)}$ .

Diese werden rekursiv w​ie folgt definiert:

${\displaystyle \delta _{0}(x,y)\quad :=\quad x=y}$   d. h. Knoten mit Abstand 0 sind gleich.

${\displaystyle \delta _{r+1}(x,y)\quad :=\quad \delta _{r}(x,y)\,\lor \,\exists z(\delta _{r}(x,z)\land (\bigvee _{R\in \sigma }\exists z_{1}\ldots \exists z_{s(R)}(Rz_{1}\ldots z_{s(R)}\land \bigvee _{1\leq i,j\leq s(R)}(z_{i}=z\land z_{j}=y))))}$

Wegen der vorausgesetzten Endlichkeit von ${\displaystyle \sigma }$ handelt es sich tatsächlich um ${\displaystyle L_{I}^{\sigma }}$ -Formeln. Die Definition der Kantenrelation im Gaifman-Graphen zeigt, dass sie das Verlangte leisten. Damit hat man auch

${\displaystyle d(a,b)>r\quad \iff \quad {\mathfrak {A}}\vDash \neg \delta _{r}(a,b)}$ .

Für Variablen ${\displaystyle {\vec {x}}:=x_{1},\ldots ,x_{n}}$ definiere

${\displaystyle \delta _{r}^{n}({\vec {x}},y):=\delta _{r}(x_{1},y)\lor \ldots \lor \delta _{r}(x_{n},y)}$ .

Offenbar gilt

${\displaystyle b\in B_{r}^{\mathfrak {A}}({\vec {a}})\quad \iff \quad {\mathfrak {A}}\vDash \delta _{r}^{n}({\vec {a}},b)}$ ,

das heißt auch über die r-Kugeln kann man in ${\displaystyle L_{I}^{\sigma }}$ sprechen.

Lokale Sätze

Wir werden lokale Formeln im Wesentlichen dadurch definieren, dass sie in einem hier zu präzisierenden Sinne auf r-Kugeln eingeschränkt sind. Zunächst erklären wir die Relativierung ${\displaystyle \varphi ^{B_{r}({\vec {x}})}({\vec {x}},{\vec {y}})}$ einer Formel ${\displaystyle \varphi ({\vec {x}},{\vec {y}})}$ dadurch, dass wir die in ${\displaystyle \varphi ({\vec {x}},{\vec {y}})}$ auftretenden Quantoren unter Verwendung obiger ${\displaystyle \delta _{r}^{n}}$ entsprechend einschränken, das heißt wir setzen rekursiv

${\displaystyle \varphi ^{B_{r}({\vec {x}})}:=\varphi }$ falls ${\displaystyle \varphi }$ atomar ist.

${\displaystyle (\neg \varphi )^{B_{r}({\vec {x}})}:=\neg (\varphi ^{B_{r}({\vec {x}})})}$

${\displaystyle (\varphi \land \psi )^{B_{r}({\vec {x}})}:=\varphi ^{B_{r}({\vec {x}})}\land \psi ^{B_{r}({\vec {x}})}}$   und entsprechend für ${\displaystyle \lor ,\rightarrow ,\leftrightarrow }$ .

${\displaystyle (\exists z\varphi )^{B_{r}({\vec {x}})}:=\exists z(\delta _{r}^{n}({\vec {x}},z)\land \varphi ^{B_{r}({\vec {x}})})}$

${\displaystyle (\forall z\varphi )^{B_{r}({\vec {x}})}:=\forall z(\delta _{r}^{n}({\vec {x}},z)\rightarrow \varphi ^{B_{r}({\vec {x}})})}$

Das i​st eine rekursive Definition über d​en Formelaufbau d​er Prädikatenlogik erster Stufe. Die rechten Seiten dieser Definitionen verwenden s​tets Relativierungen bereits erklärter u​nd einfacher aufgebauter Formeln.

Die Definitionen s​ind offenbar s​o angelegt, dass

${\displaystyle {\mathfrak {A}}\vDash \varphi ^{B_{r}({\vec {x}})}({\vec {a}},{\vec {b}})\quad \iff \quad B_{r}({\vec {a}})\vDash \varphi ({\vec {a}},{\vec {b}})}$ ,

das heißt ${\displaystyle {\mathfrak {A}}}$ erfüllt die relativierte Formel genau dann, wenn bereits die r-Kugel ${\displaystyle B_{r}({\vec {a}})}$ ein Modell für ${\displaystyle \varphi ({\vec {x}},{\vec {y}})}$ ist.

Eine Formel heißt n​un eine lokale Basisformel, w​enn sie d​ie Gestalt

${\displaystyle \exists x_{1}\ldots \exists x_{n}\bigwedge _{1\leq i<j\leq n}(\neg \delta _{2r}(x_{i},x_{j})\land \varphi ^{B_{r}(x_{i})}(x_{i}))}$

hat, wobei ${\displaystyle \varphi =\varphi (x)}$ eine Formel erster Stufe ist. Diese Formel drückt also aus, dass es in jedem Model ${\displaystyle {\mathfrak {A}}=(A,I)}$ Elemente ${\displaystyle a_{1},\ldots ,a_{n}\in A}$ gibt, die einen Abstand ${\displaystyle >2r}$ haben, so dass sich die r-Kugeln um die ${\displaystyle a_{i}}$ nicht schneiden, und dass die durch ${\displaystyle \varphi }$ beschriebene Eigenschaft lokal ist, genauer, dass bereits die r-Kugel um jedes Element ein Modell für diese Eigenschaft ist.

Schließlich heißt eine Formel lokal, wenn sie eine boolesche Kombination lokaler Basisformeln ist, das heißt mittels ${\displaystyle \neg ,\land ,\lor ,\rightarrow ,\leftrightarrow }$ aus lokalen Basisformeln zusammengesetzt ist.[2]

Formulierung des Satzes

Der Satz v​on Gaifman lautet:

Ist ${\displaystyle \sigma }$ eine endliche relationale Signatur, so ist jeder ${\displaystyle L_{I}^{\sigma }}$ -Satz in endlichen Modellen logisch äquivalent zu einem lokalen Satz.[3]

Bemerkungen

Ist der Quantorenrang des ${\displaystyle L_{I}^{\sigma }}$ -Satzes ${\displaystyle \leq k}$ , das heißt die maximale Verschachtelungstiefe von Existenz- und Allquantoren in diesem Satz ist maximal ${\displaystyle k}$ , so kann man die r-Kugeln der im Satz von Gaifman auftretenden lokalen Basissätze mit ${\displaystyle r\leq 7^{k}}$ wählen.

Allgemeiner ist jede Formel erster Stufe mit freien Variablen logisch äquivalent zu einer booleschen Kombination aus Formeln der Form ${\displaystyle \varphi ^{B_{r}({\vec {x}})}}$ und lokalen Sätzen.[4]

Aus dem Satz von Gaifman ergibt sich die Gaifman-Lokalität der Prädikatenlogik erster Stufe. Allerdings ist die Abschätzung ${\displaystyle 7^{k}}$ für das kleinste ${\displaystyle r}$ , das man für die lokalen Basissätze im Satz von Gaifman wählen kann, schwächer als die im unten angegebenen Lehrbuch von Leonid Libkin oder im Artikel zur Gaifman-Lokalität angegebenen Abschätzungen.

Einzelnachweise

1. Haim Gaifman: On local and non-local properties, Proceedings Herbrand Symposium, Logic Colloquium ´81, North Holland Verlag (1982)
2. Heinz-Dieter Ebbinghaus, Jörg Flum: Finite Model Theory, Springer-Verlag 1999, ISBN 3-540-28787-6, Seite 31
3. Heinz-Dieter Ebbinghaus, Jörg Flum: Finite Model Theory, Springer-Verlag 1999, ISBN 3-540-28787-6, Satz 2.5.1. Gaifman's Theorem
4. Leonid Libkin: Elements of Finite Model Theory, Springer-Verlag (2004), ISBN 3-540-21202-7, Theorem 4.22