99:), whereas Spoiler wants to show that they are different. The game is played in rounds. A round proceeds as follows: Spoiler chooses any element from one of the structures, and Duplicator chooses an element from the other structure. In simplified terms, the Duplicator's task is to always pick an element "similar" to the one that the Spoiler has chosen, whereas the Spoiler's task is to choose an element for which no "similar" element exists in the other structure. Duplicator wins if there exists an isomorphism between the eventual substructures chosen from the two different structures; otherwise, Spoiler wins.
40:. The main application of Ehrenfeucht–Fraïssé games is in proving the inexpressibility of certain properties in first-order logic. Indeed, Ehrenfeucht–Fraïssé games provide a complete methodology for proving inexpressibility results for
1113:
56:), since Ehrenfeucht–Fraïssé games are one of the few techniques from model theory that remain valid in the context of finite models. Other widely used techniques for proving inexpressibility results, such as the
1535:'s book chapter on Ehrenfeucht–Fraïssé games discuss applications in computer science, the methodology for proving inexpressibility results, and several simple inexpressibility proofs using this methodology.
1167:
261:
1247:
1201:
854:
784:
1414:
1390:
1366:
1342:
1295:
1271:
1011:
940:
878:
808:
709:
685:
601:
550:
496:
445:
394:
367:
316:
196:
172:
1169:. These are all equivalence relations on the class of structures with the given relation symbols. The intersection of all these relations is again an equivalence relation
916:
1498:
1478:
140:
120:
1058:
987:
658:
631:
577:
526:
472:
421:
343:
292:
735:
1434:
1318:
1031:
960:
1775:
1740:
1071:
1524:'s model theory text contains an introduction to the Ehrenfeucht–Fraïssé game, and so do Chapters 6, 7, and 13 of Rosenstein's book on
1586:
72:
33:
1122:
216:
96:
1218:
1172:
1808:
I, Miroslav Benda, Transactions of the
American Mathematical Society, Vol. 250 (Jun 1979), pp. 47 – 90 (44 pages)
1297:
are elementarily equivalent. If the set of relation symbols being considered is finite, the converse is also true.
1567:
Computer
Science Logic: 6th Workshop, CSL'92, San Miniato, Italy, September 28 - October 2, 1992. Selected Papers
1542:
are certain equivalence relations and the derivative provides for a generalization of standard model theory.
92:
37:
1730:
1528:. A simple example of the Ehrenfeucht–Fraïssé game is given in one of Ivars Peterson's MathTrek columns.
203:
199:
1821:
1445:
813:
743:
1449:
1395:
1371:
1347:
1323:
1276:
1252:
992:
921:
859:
789:
690:
666:
582:
531:
477:
426:
375:
348:
297:
177:
153:
1559:
883:
1501:
1453:
57:
49:
45:
1521:
1702:
1799:
1771:
1736:
1582:
1483:
1463:
41:
1726:
1416:
can be shown equivalent by providing a winning strategy for
Duplicator, then this shows that
125:
105:
1781:
1592:
1574:
1036:
965:
636:
609:
555:
504:
450:
399:
321:
270:
71:
for finite variable logics; extensions are powerful enough to characterise definability in
1785:
1767:
1596:
1570:
1525:
53:
714:
1759:
1505:
1419:
1303:
1016:
945:
207:
64:
29:
1648:
1538:
Ehrenfeucht–Fraïssé games are the basis for the operation of derivative on modeloids.
1815:
1532:
1713:
1755:
1714:
Course on combinatorial games in finite model theory by
Phokion Kolaitis (.ps file)
1457:
1448:
used in the
Ehrenfeucht–Fraïssé game to verify elementary equivalence was given by
21:
1060:. Duplicator wins if these structures are the same; Spoiler wins if they are not.
1667:
83:
The main idea behind the game is that we have two structures, and two players –
68:
17:
1560:"An Ehrenfeucht–Fraïssé game for fixpoint logic and stratified fixpoint logic"
263:
to be a game between two players, Spoiler and
Duplicator, played as follows:
63:
Ehrenfeucht–Fraïssé-like games can also be defined for other logics, such as
1578:
1649:
An application of games to the completeness problem for formalized theories
1805:
1539:
1108:{\displaystyle {\mathfrak {A}}\ {\overset {n}{\sim }}\ {\mathfrak {B}}}
1211:
It is easy to prove that if
Duplicator wins this game for all finite
1754:
Grädel, Erich; Kolaitis, Phokion G.; Libkin, Leonid; Maarten, Marx;
1766:. Texts in Theoretical Computer Science. An EATCS Series. Berlin:
1681:, Bruno Poizat, tr. Moses Klein, New York: Springer-Verlag, 2000.
1460:. Other usual names are Eloise and Abelard (and often denoted by
740:
At the conclusion of the game, we have chosen distinct elements
1668:
Stanford
Encyclopedia of Philosophy, entry on Logic and Games.
44:. In this role, these games are of particular importance in
1802:
at MATH EXPLORERS' CLUB, Cornell
Department of Mathematics.
28:(also called back-and-forth games) is a technique based on
1610:
Sur une nouvelle classification des systèmes de relations
1693:, Joseph G. Rosenstein, New York: Academic Press, 1982.
91:. Duplicator wants to show that the two structures are
48:
and its applications in computer science (specifically
1629:
Sur quelques classifications des systèmes de relations
1162:{\displaystyle G_{n}({\mathfrak {A}},{\mathfrak {B}})}
256:{\displaystyle G_{n}({\mathfrak {A}},{\mathfrak {B}})}
1486:
1466:
1436:
is inexpressible in the logic captured by this game.
1422:
1398:
1374:
1350:
1326:
1306:
1279:
1255:
1221:
1175:
1125:
1074:
1039:
1019:
995:
968:
948:
924:
886:
862:
816:
792:
746:
717:
693:
669:
639:
612:
585:
558:
534:
507:
480:
453:
429:
402:
378:
351:
324:
300:
273:
219:
180:
156:
128:
108:
1631:, Roland Fraïssé, thesis, Paris, 1953; published in
1569:. Lecture Notes in Computer Science. Vol. 702.
213:. We can then define the Ehrenfeucht–Fraïssé game
1242:{\displaystyle {\mathfrak {A}}\sim {\mathfrak {B}}}
1196:{\displaystyle {\mathfrak {A}}\sim {\mathfrak {B}}}
663:Spoiler and Duplicator continue to pick members of
1633:Publications Scientifiques de l'Université d'Alger
1492:
1472:
1428:
1408:
1384:
1360:
1336:
1312:
1289:
1265:
1241:
1195:
1161:
1107:
1052:
1025:
1005:
981:
954:
934:
910:
872:
848:
802:
778:
729:
703:
679:
652:
625:
595:
571:
544:
520:
490:
466:
439:
415:
388:
361:
337:
310:
286:
255:
190:
166:
134:
122:(which is an ordinal – usually a finite number or
114:
267:The first player, Spoiler, picks either a member
880:. We therefore have two structures on the set
1456:. The names Spoiler and Duplicator are due to
1452:in his thesis; it was formulated as a game by
660:in the model from which Spoiler did not pick.
8:
905:
887:
102:The game lasts for a fixed number of steps
1800:Six Lectures on Ehrenfeucht-Fraïssé games
1485:
1465:
1421:
1400:
1399:
1397:
1376:
1375:
1373:
1352:
1351:
1349:
1328:
1327:
1325:
1305:
1281:
1280:
1278:
1257:
1256:
1254:
1233:
1232:
1223:
1222:
1220:
1187:
1186:
1177:
1176:
1174:
1150:
1149:
1140:
1139:
1130:
1124:
1099:
1098:
1085:
1076:
1075:
1073:
1044:
1038:
1018:
997:
996:
994:
973:
967:
947:
926:
925:
923:
885:
864:
863:
861:
840:
821:
815:
794:
793:
791:
770:
751:
745:
716:
695:
694:
692:
671:
670:
668:
644:
638:
617:
611:
587:
586:
584:
563:
557:
536:
535:
533:
512:
506:
482:
481:
479:
458:
452:
431:
430:
428:
407:
401:
380:
379:
377:
353:
352:
350:
329:
323:
302:
301:
299:
278:
272:
244:
243:
234:
233:
224:
218:
182:
181:
179:
158:
157:
155:
150:Suppose that we are given two structures
127:
107:
1764:Finite model theory and its applications
1762:; Venema, Yde; Weinstein, Scott (2007).
1703:Example of the Ehrenfeucht-Fraïssé game.
1550:
447:; otherwise, Duplicator picks a member
1727:"Chapter 6: Ehrenfeucht–Fraïssé Games"
7:
1401:
1377:
1353:
1329:
1282:
1258:
1234:
1224:
1188:
1178:
1151:
1141:
1100:
1077:
998:
927:
865:
795:
696:
672:
588:
537:
483:
432:
381:
354:
303:
245:
235:
183:
159:
1487:
1467:
849:{\displaystyle b_{1},\dots ,b_{n}}
779:{\displaystyle a_{1},\dots ,a_{n}}
14:
1512:, or alternatively Eve and Adam.
1504:, a naming scheme introduced by
1207:Equivalence and inexpressibility
60:, do not work in finite models.
1409:{\displaystyle {\mathfrak {B}}}
1385:{\displaystyle {\mathfrak {A}}}
1361:{\displaystyle {\mathfrak {B}}}
1337:{\displaystyle {\mathfrak {A}}}
1290:{\displaystyle {\mathfrak {B}}}
1266:{\displaystyle {\mathfrak {A}}}
1006:{\displaystyle {\mathfrak {B}}}
935:{\displaystyle {\mathfrak {A}}}
873:{\displaystyle {\mathfrak {B}}}
803:{\displaystyle {\mathfrak {A}}}
704:{\displaystyle {\mathfrak {B}}}
680:{\displaystyle {\mathfrak {A}}}
596:{\displaystyle {\mathfrak {B}}}
545:{\displaystyle {\mathfrak {A}}}
491:{\displaystyle {\mathfrak {A}}}
440:{\displaystyle {\mathfrak {B}}}
389:{\displaystyle {\mathfrak {A}}}
362:{\displaystyle {\mathfrak {B}}}
311:{\displaystyle {\mathfrak {A}}}
191:{\displaystyle {\mathfrak {B}}}
167:{\displaystyle {\mathfrak {A}}}
1156:
1136:
989:, and the other induced from
911:{\displaystyle \{1,\dots ,n\}}
501:Spoiler picks either a member
372:If Spoiler picked a member of
250:
230:
95:(satisfy the same first-order
73:existential second-order logic
1:
1735:. Springer. pp. 91–112.
1531:Phokion Kolaitis' slides and
606:Duplicator picks an element
396:, Duplicator picks a member
202:symbols and the same set of
32:for determining whether two
50:computer aided verification
1838:
1565:. In Börger, Egon (ed.).
1679:A Course in Model Theory
1619:(1950), 1022–1024.
1493:{\displaystyle \forall }
1473:{\displaystyle \exists }
26:Ehrenfeucht–Fraïssé game
1653:Fundamenta Mathematicae
1579:10.1007/3-540-56992-8_8
1115:if Duplicator wins the
135:{\displaystyle \omega }
115:{\displaystyle \gamma }
93:elementarily equivalent
38:elementarily equivalent
1732:Descriptive Complexity
1725:Neil Immerman (1999).
1658:(1961), 129–141.
1494:
1474:
1430:
1410:
1386:
1362:
1338:
1314:
1291:
1267:
1243:
1197:
1163:
1109:
1054:
1027:
1007:
983:
956:
936:
912:
874:
850:
804:
780:
731:
705:
681:
654:
627:
597:
573:
546:
522:
492:
468:
441:
417:
390:
363:
339:
312:
288:
257:
206:symbols, and a fixed
192:
168:
136:
116:
1639:(1954), 35–182.
1495:
1475:
1446:back-and-forth method
1431:
1411:
1387:
1363:
1339:
1315:
1292:
1268:
1244:
1198:
1164:
1110:
1068:we define a relation
1055:
1053:{\displaystyle b_{i}}
1028:
1008:
984:
982:{\displaystyle a_{i}}
957:
937:
913:
875:
851:
805:
781:
732:
706:
682:
655:
653:{\displaystyle b_{2}}
628:
626:{\displaystyle a_{2}}
598:
574:
572:{\displaystyle b_{2}}
547:
523:
521:{\displaystyle a_{2}}
493:
469:
467:{\displaystyle a_{1}}
442:
418:
416:{\displaystyle b_{1}}
391:
364:
340:
338:{\displaystyle b_{1}}
313:
289:
287:{\displaystyle a_{1}}
258:
193:
169:
137:
117:
1573:. pp. 100–114.
1484:
1464:
1420:
1396:
1372:
1348:
1324:
1304:
1277:
1253:
1219:
1173:
1123:
1072:
1037:
1017:
1013:via the map sending
993:
966:
946:
942:via the map sending
922:
884:
860:
814:
790:
744:
715:
691:
667:
637:
610:
583:
556:
532:
505:
478:
451:
427:
400:
376:
349:
322:
298:
271:
217:
178:
154:
126:
106:
1558:Bosse, Uwe (1993).
1502:Heloise and Abelard
1454:Andrzej Ehrenfeucht
918:, one induced from
730:{\displaystyle n-2}
58:compactness theorem
46:finite model theory
1651:, A. Ehrenfeucht,
1612:, Roland Fraïssé,
1490:
1470:
1426:
1406:
1382:
1358:
1334:
1310:
1287:
1263:
1239:
1193:
1159:
1105:
1050:
1023:
1003:
979:
952:
932:
908:
870:
846:
800:
776:
727:
701:
677:
650:
623:
593:
569:
542:
518:
488:
464:
437:
413:
386:
359:
335:
308:
284:
253:
188:
164:
132:
112:
1777:978-3-540-00428-8
1742:978-0-387-98600-5
1429:{\displaystyle Q}
1313:{\displaystyle Q}
1097:
1093:
1084:
1026:{\displaystyle i}
955:{\displaystyle i}
42:first-order logic
1829:
1789:
1747:
1746:
1722:
1716:
1711:
1705:
1700:
1694:
1691:Linear Orderings
1688:
1682:
1676:
1670:
1665:
1659:
1646:
1640:
1626:
1620:
1607:
1601:
1600:
1564:
1555:
1499:
1497:
1496:
1491:
1479:
1477:
1476:
1471:
1435:
1433:
1432:
1427:
1415:
1413:
1412:
1407:
1405:
1404:
1391:
1389:
1388:
1383:
1381:
1380:
1367:
1365:
1364:
1359:
1357:
1356:
1344:but not true of
1343:
1341:
1340:
1335:
1333:
1332:
1319:
1317:
1316:
1311:
1296:
1294:
1293:
1288:
1286:
1285:
1272:
1270:
1269:
1264:
1262:
1261:
1248:
1246:
1245:
1240:
1238:
1237:
1228:
1227:
1202:
1200:
1199:
1194:
1192:
1191:
1182:
1181:
1168:
1166:
1165:
1160:
1155:
1154:
1145:
1144:
1135:
1134:
1114:
1112:
1111:
1106:
1104:
1103:
1095:
1094:
1086:
1082:
1081:
1080:
1059:
1057:
1056:
1051:
1049:
1048:
1032:
1030:
1029:
1024:
1012:
1010:
1009:
1004:
1002:
1001:
988:
986:
985:
980:
978:
977:
961:
959:
958:
953:
941:
939:
938:
933:
931:
930:
917:
915:
914:
909:
879:
877:
876:
871:
869:
868:
855:
853:
852:
847:
845:
844:
826:
825:
809:
807:
806:
801:
799:
798:
785:
783:
782:
777:
775:
774:
756:
755:
736:
734:
733:
728:
710:
708:
707:
702:
700:
699:
686:
684:
683:
678:
676:
675:
659:
657:
656:
651:
649:
648:
632:
630:
629:
624:
622:
621:
602:
600:
599:
594:
592:
591:
578:
576:
575:
570:
568:
567:
551:
549:
548:
543:
541:
540:
527:
525:
524:
519:
517:
516:
497:
495:
494:
489:
487:
486:
473:
471:
470:
465:
463:
462:
446:
444:
443:
438:
436:
435:
422:
420:
419:
414:
412:
411:
395:
393:
392:
387:
385:
384:
368:
366:
365:
360:
358:
357:
344:
342:
341:
336:
334:
333:
317:
315:
314:
309:
307:
306:
293:
291:
290:
285:
283:
282:
262:
260:
259:
254:
249:
248:
239:
238:
229:
228:
197:
195:
194:
189:
187:
186:
173:
171:
170:
165:
163:
162:
141:
139:
138:
133:
121:
119:
118:
113:
1837:
1836:
1832:
1831:
1830:
1828:
1827:
1826:
1812:
1811:
1796:
1778:
1768:Springer-Verlag
1760:Vardi, Moshe Y.
1753:
1750:
1743:
1724:
1723:
1719:
1712:
1708:
1701:
1697:
1689:
1685:
1677:
1673:
1666:
1662:
1647:
1643:
1627:
1623:
1608:
1604:
1589:
1571:Springer-Verlag
1562:
1557:
1556:
1552:
1548:
1518:
1516:Further reading
1482:
1481:
1462:
1461:
1442:
1418:
1417:
1394:
1393:
1370:
1369:
1346:
1345:
1322:
1321:
1302:
1301:
1275:
1274:
1251:
1250:
1217:
1216:
1209:
1171:
1170:
1126:
1121:
1120:
1070:
1069:
1040:
1035:
1034:
1015:
1014:
991:
990:
969:
964:
963:
944:
943:
920:
919:
882:
881:
858:
857:
836:
817:
812:
811:
788:
787:
766:
747:
742:
741:
713:
712:
689:
688:
665:
664:
640:
635:
634:
613:
608:
607:
581:
580:
559:
554:
553:
530:
529:
508:
503:
502:
476:
475:
454:
449:
448:
425:
424:
403:
398:
397:
374:
373:
347:
346:
325:
320:
319:
296:
295:
274:
269:
268:
220:
215:
214:
198:, each with no
176:
175:
152:
151:
148:
124:
123:
104:
103:
81:
65:fixpoint logics
54:database theory
12:
11:
5:
1835:
1833:
1825:
1824:
1814:
1813:
1810:
1809:
1803:
1795:
1794:External links
1792:
1791:
1790:
1776:
1749:
1748:
1741:
1717:
1706:
1695:
1683:
1671:
1660:
1641:
1621:
1614:Comptes Rendus
1602:
1587:
1549:
1547:
1544:
1517:
1514:
1506:Wilfrid Hodges
1489:
1469:
1450:Roland Fraïssé
1441:
1438:
1425:
1403:
1379:
1355:
1331:
1309:
1300:If a property
1284:
1260:
1236:
1231:
1226:
1208:
1205:
1190:
1185:
1180:
1158:
1153:
1148:
1143:
1138:
1133:
1129:
1102:
1092:
1089:
1079:
1062:
1061:
1047:
1043:
1022:
1000:
976:
972:
951:
929:
907:
904:
901:
898:
895:
892:
889:
867:
843:
839:
835:
832:
829:
824:
820:
797:
773:
769:
765:
762:
759:
754:
750:
738:
726:
723:
720:
698:
674:
661:
647:
643:
620:
616:
604:
590:
566:
562:
539:
515:
511:
499:
485:
461:
457:
434:
410:
406:
383:
370:
356:
332:
328:
305:
281:
277:
252:
247:
242:
237:
232:
227:
223:
208:natural number
185:
161:
147:
144:
131:
111:
80:
77:
30:game semantics
20:discipline of
13:
10:
9:
6:
4:
3:
2:
1834:
1823:
1820:
1819:
1817:
1807:
1804:
1801:
1798:
1797:
1793:
1787:
1783:
1779:
1773:
1769:
1765:
1761:
1757:
1756:Spencer, Joel
1752:
1751:
1744:
1738:
1734:
1733:
1728:
1721:
1718:
1715:
1710:
1707:
1704:
1699:
1696:
1692:
1687:
1684:
1680:
1675:
1672:
1669:
1664:
1661:
1657:
1654:
1650:
1645:
1642:
1638:
1634:
1630:
1625:
1622:
1618:
1615:
1611:
1606:
1603:
1598:
1594:
1590:
1588:3-540-56992-8
1584:
1580:
1576:
1572:
1568:
1561:
1554:
1551:
1545:
1543:
1541:
1536:
1534:
1533:Neil Immerman
1529:
1527:
1526:linear orders
1523:
1520:Chapter 1 of
1515:
1513:
1511:
1507:
1503:
1459:
1455:
1451:
1447:
1439:
1437:
1423:
1307:
1298:
1229:
1214:
1206:
1204:
1183:
1146:
1131:
1127:
1118:
1090:
1087:
1067:
1045:
1041:
1020:
974:
970:
949:
902:
899:
896:
893:
890:
841:
837:
833:
830:
827:
822:
818:
771:
767:
763:
760:
757:
752:
748:
739:
724:
721:
718:
662:
645:
641:
618:
614:
605:
564:
560:
513:
509:
500:
459:
455:
408:
404:
371:
330:
326:
279:
275:
266:
265:
264:
240:
225:
221:
212:
209:
205:
201:
145:
143:
129:
109:
100:
98:
94:
90:
86:
78:
76:
74:
70:
66:
61:
59:
55:
51:
47:
43:
39:
35:
31:
27:
23:
19:
1822:Model theory
1763:
1731:
1720:
1709:
1698:
1690:
1686:
1678:
1674:
1663:
1655:
1652:
1644:
1636:
1632:
1628:
1624:
1616:
1613:
1609:
1605:
1566:
1553:
1537:
1530:
1519:
1510:Model Theory
1509:
1508:in his book
1458:Joel Spencer
1443:
1299:
1212:
1210:
1116:
1065:
1063:
552:or a member
318:or a member
210:
149:
101:
88:
84:
82:
69:pebble games
62:
25:
22:model theory
18:mathematical
15:
1635:, series A
1320:is true of
1215:, that is,
1119:-move game
737:more steps.
1786:1133.03001
1597:0808.03024
1546:References
146:Definition
89:Duplicator
34:structures
1806:Modeloids
1540:Modeloids
1488:∀
1468:∃
1230:∼
1184:∼
1088:∼
1064:For each
897:…
831:…
761:…
722:−
130:ω
110:γ
97:sentences
79:Main idea
1816:Category
1500:) after
204:relation
200:function
1440:History
1249:, then
85:Spoiler
16:In the
1784:
1774:
1739:
1595:
1585:
1522:Poizat
1368:, but
1096:
1083:
24:, the
1563:(PDF)
1772:ISBN
1737:ISBN
1583:ISBN
1480:and
1444:The
1392:and
1273:and
810:and
711:for
687:and
174:and
87:and
67:and
52:and
36:are
1782:Zbl
1617:230
1593:Zbl
1575:doi
1033:to
962:to
856:of
786:of
633:or
579:of
528:of
474:of
423:of
345:of
294:of
142:).
1818::
1780:.
1770:.
1758:;
1729:.
1656:49
1591:.
1581:.
1203:.
75:.
1788:.
1745:.
1637:1
1599:.
1577::
1424:Q
1402:B
1378:A
1354:B
1330:A
1308:Q
1283:B
1259:A
1235:B
1225:A
1213:n
1189:B
1179:A
1157:)
1152:B
1147:,
1142:A
1137:(
1132:n
1128:G
1117:n
1101:B
1091:n
1078:A
1066:n
1046:i
1042:b
1021:i
999:B
975:i
971:a
950:i
928:A
906:}
903:n
900:,
894:,
891:1
888:{
866:B
842:n
838:b
834:,
828:,
823:1
819:b
796:A
772:n
768:a
764:,
758:,
753:1
749:a
725:2
719:n
697:B
673:A
646:2
642:b
619:2
615:a
603:.
589:B
565:2
561:b
538:A
514:2
510:a
498:.
484:A
460:1
456:a
433:B
409:1
405:b
382:A
369:.
355:B
331:1
327:b
304:A
280:1
276:a
251:)
246:B
241:,
236:A
231:(
226:n
222:G
211:n
184:B
160:A
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.