Игра Эренфойхта — Фраиса

Игры Эренфойхта — Фраиса (иногда челночные игры англ. back-and-forth games) — это техника определения, являются ли две структуры элементарно эквивалентными. Основное приложение игр Эренфойхта — Фраиса — доказательство невозможности выразить определённые свойства в логике первого порядка. Более того, игры Эренфойхта — Фраиса дают полную методологию для доказательства невозможности выразить свойства в логике первого порядка. В такой роли эти игры особенно важны в теории конечных моделей и её приложениях в информатике (особенно в компьютерной верификации и теории баз данных), поскольку игры Эренфойхта — Фраиса являются одной из немногочисленных техник в теории моделей, которые остаются верными в контексте конечных моделей. Другие широко используемые техники для доказательства невозможности выразить свойства, такие как теорема о компактности, не работает для конечных моделей.

Игры, подобные игре Эренфойхта — Фраиса, могут быть также определены для других логик, таких как логик фиксированной точки и фишечные игры для логик с конечным числом переменных. Расширения достаточно мощны, чтобы описать определимость в экзистенциальной логике второго порядка.

Основная идея

Основная идея игры заключается в том, что мы имеем две структуры и два игрока (определены ниже). Один из игроков хочет показать, что эти две структуры отличны, в то время как другой игрок хочет показать, что они элементарно эквивалентны (удовлетворяют тем же предложения первого порядка). Игра ведётся поочерёдно по раундам. Раунд протекает следующим образом: Сначала первый игрок Новатор выбирает любой элемент из одной из структур, а другой игрок выбирает элемент из другой структуры. Целью второго игрока всегда является выбор элемента, который «похож» на элемент, выбранный Новатором. Второй игрок (Консерватор) выигрывает, если существует изоморфизм между выбранными элементами в двух различных структурах.

Игра завершается за фиксированное число шагов ($\gamma$) (ординал, но обычно конечное число или $\omega$).

Определение

Предположим, что нам даны две структуры ${\mathfrak {A}}$ and ${\mathfrak {B}}$ с одинаковыми множеством отношений символов и дано фиксированное натуральное число n. Мы можем тогда определить игру Эренфойхта — Фраиса $G_{n}({\mathfrak {A}},{\mathfrak {B}})$ как игру между двумя игроками, Новатором и Консерватором, следующим образом:

1. Первый игрок, Новатор, выбирает либо члена $a_{1}$ структуры ${\mathfrak {A}}$, или члена $b_{1}$ структуры ${\mathfrak {B}}$.
2. Если Новатор выбирает члена структуры ${\mathfrak {A}}$, Консерватор выбирает члена $b_{1}$ структуры ${\mathfrak {B}}$. В противном случае Консерватор выбирает члена $a_{1}$ структуры ${\mathfrak {A}}$.
3. Новатор выбирает либо члена $a_{2}$ структуры ${\mathfrak {A}}$ или члена $b_{2}$ структуры ${\mathfrak {B}}$.
4. Консерватор выбирает элемент $a_{2}$ или $b_{2}$ в модели, из которой Новатор не выбирал.
5. Новатор и Консерватор продолжают выбирать члены из структур ${\mathfrak {A}}$ и ${\mathfrak {B}}$ ещё на $n-2$ шагах.
6. Под конец игры мы выбрали различные элементы $a_{1},\dots ,a_{n}$ структуры ${\mathfrak {A}}$ и $b_{1},\dots ,b_{n}$ структуры ${\mathfrak {B}}$. Мы поэтому имеем две структуры на множестве $\{1,\dots ,n\}$, одна получена из структуры ${\mathfrak {A}}$ отображением $i$ в $a_{i}$, а другая получена из ${\mathfrak {B}}$ отражением $i$ в $b_{i}$. Консерватор выигрывает, если эти структуры одинаковы. Новатор выигрывает, если они не одинаковы.

Для любого n мы определяем отношение ${\mathfrak {A}}{\stackrel {n}{\sim }}{\mathfrak {B}}$, если Консерватор выигрывает в игре с n ходами $G_{n}({\mathfrak {A}},{\mathfrak {B}})$. Это все отношения эквивалентности на классе структур с заданными символами отношений. Пересечение всех этих отношений снова является отношением эквивалентности ${\mathfrak {A}}\sim {\mathfrak {B}}$.

Легко доказать, что если Консерватор выигрывает игру для всех n, то есть ${\mathfrak {A}}\sim {\mathfrak {B}}$, то ${\mathfrak {A}}$ и ${\mathfrak {B}}$ элементарно эквивалентны. Если множество отношений символов конечно, обратное тоже верно.

История

Челночный метод (или метод подбора), использованный в игре Эренфойхта — Фраиса для проверки элементарной эквивалентности предложил Роланд Фрейсе в своей диссертации. Метод сформулировал в виде игры Анджей Эренфойхт. Названия Spoiler и Duplicator дал Joel Spencer. Также используются названия Eloise и Abelard (и обозначаются часто $\exists$ и $\forall$) по именам Элоиза и Абеляр, по схеме именований, предложенной Вильфридом Ходжисом в его книге Теория моделей.

Литература для дальнейшего чтения

Глава 1 книги Пуазы по теории моделей содержат введение в игру Эренфойхта — Фраиса. Главы 6, 7 и 13 книги Розенштейна о линейных порядках также содержит введение в игру. Простые примеры игры Эренфойхта — Фраиса есть в одной из колонок MathTrek Иварса Петерсона.

Введение в игру Эренфойхта — Фраиса и некоторые простые примеры этой игры можно найти в книге Верещагина и Шеня.

Слайды Фокион Колайтиса и глава книги Нейла Иммермана об играх Эренфойхта — Фраиса обсуждают приложения в информатике, методологической теореме для доказательства невыразимости и некоторые простые доказательства невыразимости с помощью этой методологии.

Ссылки

• Six Lectures Ehrenfeucht-Fraïssé games at MATH EXPLORERS' CLUB, Cornell Department of Mathematics.
• Modeloids I, Miroslav Benda, Transactions of the American Mathematical Society, Vol. 250 (Jun 1979), pp. 47 – 90 (44 pages)