„Ehrenfeucht-Fraïssé-Spiele“ – Versionsunterschied

Ehrenfeucht-Fraïssé-Spiele (EF-Spiele) sind eine Beweistechnik der Modelltheorie. Durch EF-Spiele lässt sich die Äquivalenz zweier Strukturen zeigen bzw. widerlegen. Sie wurden von Andrzej Ehrenfeucht auf Grundlage der theoretischen Arbeit des Mathematikers Roland Fraïssé entwickelt.

Ein EF-Spiel wird von zwei Spielern gespielt, gewöhnlich bezeichnet mit Spoiler und Duplicator (nach Joel Spencer) oder Samson und Delilah (nach Neil Immerman) .

Definition

Seien ${\mathfrak {A}},{\mathfrak {B}}$ zwei Strukturen, $n\in \mathbb {N}$.

Das EF-Spiel $G_{n}({\mathfrak {A}},{\mathfrak {B}})$ hat n Runden.

• in jeder Runde i (i<n) wählt zunächst Samson ein beliebiges $a_{i}\in {\mathfrak {A}}$ oder ein $b_{i}\in {\mathfrak {B}}$, welches noch nicht zuvor gewählt wurde
• falls Samson ein Element aus ${\mathfrak {A}}$ gewählt hat, wählt daraufhin Delilah ein beliebiges $b_{i}\in {\mathfrak {B}}$, sonst ein $a_{i}\in {\mathfrak {A}}$

Nach n Runden resultiert eine Menge von 2-Tupeln $\{(a_{0},b_{0}),\ \ldots \ ,(a_{n-1},b_{n-1})\}\subseteq {\mathfrak {A}}\times {\mathfrak {B}}$.

• Falls durch diese Menge ein partieller Isomorphismus $\varphi :{\mathfrak {A}}\rightarrow {\mathfrak {B}}$ definiert wird, hat Delilah gewonnen.

Per Definition gewinnt Delilah das Spiel $G_{n}({\mathfrak {A}},{\mathfrak {B}})$, falls sie eine zwingende Gewinnstrategie hat.

Satz

Zwei Strukturen ${\mathfrak {A}},{\mathfrak {B}}$ sind n-äquivalent, ${\mathfrak {A}}\equiv _{n}{\mathfrak {B}}\iff$ Delilah gewinnt $G_{n}({\mathfrak {A}},{\mathfrak {B}})$.

Korollar

$\forall n\in \mathbb {N} :{\mathfrak {A}}\equiv _{n}{\mathfrak {B}}\iff {\mathfrak {A}}$ und ${\mathfrak {B}}$ sind elementar äquivalent.