Введение
В математической дисциплине теории моделей игра Эренфюхта — Фрейссе (также называемая играми «туда и обратно») — это метод, основанный на семантике игр, для определения элементарной эквивалентности двух структур. Основное применение игры Эренфюхта — Фрейссе заключается в доказательстве невыразимости определенных свойств в логике первого порядка. Фактически, игра Эренфюхта — Фрейссе предоставляет полную методологию для доказательства результатов о невыразимости в логике первого порядка. В этом качестве эти игры особенно важны в теории конечных моделей и её приложениях в информатике (в частности, в компьютерной верификации и теории баз данных), поскольку игра Эренфюхта — Фрейссе является одним из немногих методов теории моделей, которые остаются применимыми к конечным моделям. Другие широко используемые методы доказательства невыразимости, такие как теорема о компактности, не работают для конечных моделей. Игры, подобные игре Эренфюхта — Фрейссе, также могут быть определены для других логик, таких как логики с фиксированными точками и игры с камешками для логик с конечным числом переменных; расширения достаточно мощны, чтобы характеризовать определимость в экзистенциальной логике второго порядка.
is a technique based on game semantics for determining whether two structures
are elementarily equivalent. 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 first order logic. In this role, these games are of particular importance in finite model theory and its applications in computer science (specifically computer aided verification and database theory), 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 compactness theorem, do not work in finite models. Ehrenfeucht–Fraïssé like games can also be defined for other logics, such as fixpoint logics and pebble games for finite variable logics; extensions are powerful enough to characterise definability in existential second order logic.
Основная идея
Основная идея игры заключается в том, что у нас есть две структуры и два игрока – Спойлер и Дубликатор. Дубликатор стремится доказать, что две структуры элементарно эквивалентны (то есть удовлетворяют одним и тем же формулам первого порядка), а Спойлер – что они различны. Игра проходит в раундах. В каждом раунде Спойлер выбирает произвольный элемент из одной из структур, а Дубликатор – элемент из другой структуры. Говоря упрощенно, задача Дубликатора – всегда выбирать элемент, "похожий" на выбранный Спойлером, а задача Спойлера – выбрать элемент, для которого не существует "похожего" элемента в другой структуре. Дубликатор выигрывает, если существует изоморфизм между образовавшимися подструктурами, выбранными из двух исходных структур; в противном случае выигрывает Спойлер. Игра длится фиксированное число ходов (которое является ординалом – обычно конечным числом или ω).
Эквивалентность и невыразимость
Легко доказать, что если Дупликатор выигрывает эту игру для всех конечных n, то есть , то структуры и элементарно эквивалентны. Если рассматриваемый набор символов отношений конечен, то верно и обратное утверждение. Если свойство истинно для структуры , но не истинно для структуры , но и можно показать эквивалентными, предоставив выигрышную стратегию для Дупликатора, то это показывает, что свойство не выразимо в логике, определяемой этой игрой.