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

Игры Эренфойхта — Фраиса (иногда челночные игры Шаблон:Lang-en) — это техника определения, являются ли две Шаблон:Не переведено 5 Шаблон:Не переведено 5. Основное приложение игр Эренфойхта — Фраиса — доказательство невозможности выразить определённые свойства в логике первого порядка. Более того, игры Эренфойхта — Фраиса дают полную методологию для доказательства невозможности выразить свойства в логике первого порядка. В такой роли эти игры особенно важны в Шаблон:Не переведено 5 и её приложениях в информатике (особенно в Шаблон:Не переведено 5 и Шаблон:Не переведено 5), поскольку игры Эренфойхта — Фраиса являются одной из немногочисленных техник в теории моделей, которые остаются верными в контексте конечных моделей. Другие широко используемые техники для доказательства невозможности выразить свойства, такие как теорема о компактности, не работает для конечных моделей.

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

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

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

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

Определение

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

1. Первый игрок, Новатор, выбирает либо члена $a_1$ структуры $𝔄$, или члена $b_1$ структуры $𝔅$.
2. Если Новатор выбирает члена структуры $𝔄$, Консерватор выбирает члена $b_1$ структуры $𝔅$. В противном случае Консерватор выбирает члена $a_1$ структуры $𝔄$.
3. Новатор выбирает либо члена $a_2$ структуры $𝔄$ или члена $b_2$ структуры $𝔅$.
4. Консерватор выбирает элемент $a_2$ или $b_2$ в модели, из которой Новатор не выбирал.
5. Новатор и Консерватор продолжают выбирать члены из структур $𝔄$ и $𝔅$ ещё на $n-2$ шагах.
6. Под конец игры мы выбрали различные элементы $a_1,\dots ,a_n$ структуры $𝔄$ и $b_1,\dots ,b_n$ структуры $𝔅$. Мы поэтому имеем две структуры на множестве $\{1,\dots ,n\}$, одна получена из структуры $𝔄$ отображением $i$ в $a_i$, а другая получена из $𝔅$ отражением $i$ в $b_i$. Консерватор выигрывает, если эти структуры одинаковы. Новатор выигрывает, если они не одинаковы.

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

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

История

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

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

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

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

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

Литература

• Шаблон:Книга
• Шаблон:Книга
• Шаблон:Статья
• Шаблон:Книга Опубликовано в
  • Шаблон:Книга
• Шаблон:Статья
• Шаблон:Книга
• Шаблон:Книга
• Шаблон:Книга
• Шаблон:Книга

Ссылки

• 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)