Игры Эренфойхта — Фраиса (иногда челночные игры ) — техника определения, являются ли две .
Основное приложение игр Эренфойхта — Фраиса — доказательство невозможности выразить определённые свойства в логике первого порядка. Более того, игры Эренфойхта — Фраиса дают полную методологию для доказательства невозможности выразить свойства в логике первого порядка. В такой роли эти игры особенно важны в и её приложениях в информатике (особенно в и ), поскольку игры Эренфойхта — Фраиса являются одной из немногочисленных техник в теории моделей, которые остаются верными в контексте конечных моделей. Другие широко используемые техники для доказательства невозможности выразить свойства, такие как теорема о компактности, не работает для конечных моделей.
Игры, подобные игре Эренфойхта — Фраиса, могут быть также определены для других логик, таких как и фишечные игры для логик с конечным числом переменных. Расширения достаточно мощны, чтобы описать определимость в экзистенциальной логике второго порядка.
Основная идея Основная идея игры заключается в том, что мы имеем две структуры и два игрока (определены ниже). Один из игроков хочет показать, что эти две структуры отличны, в то время как другой игрок хочет показать, что они (удовлетворяют тем же предложения первого порядка). Игра ведётся поочерёдно по раундам. Раунд протекает следующим образом: Сначала первый игрок НоваторИспользуется терминология из книги Верещагина и Шеня . В английском варианте Новатор=Spoiler, Консерватор=Duplicator. В книге игра называется игрой Эренфойхта и приведено несколько примеров простых игр для понимания идеи. выбирает любой элемент из одной из структур, а другой игрок выбирает элемент из другой структуры. Целью второго игрока всегда является выбор элемента, который «похож» на элемент, выбранный Новатором. Второй игрок (Консерватор) выигрывает, если существует изоморфизм между выбранными элементами в двух различных структурах.
Игра завершается за фиксированное число шагов () (ординал, но обычно конечное число или ).
Определение Предположим, что нам даны две структуры and с одинаковыми множеством отношений символов и дано фиксированное натуральное число n. Мы можем тогда определить игру Эренфойхта — Фраиса как игру между двумя игроками, Новатором и Консерватором, следующим образом: Первый игрок, Новатор, выбирает либо члена структуры , или члена структуры . Если Новатор выбирает члена структуры , Консерватор выбирает члена структуры . В противном случае Консерватор выбирает члена структуры . Новатор выбирает либо члена структуры или члена структуры . Консерватор выбирает элемент или в модели, из которой Новатор не выбирал. Новатор и Консерватор продолжают выбирать члены из структур и ещё на шагах. Под конец игры мы выбрали различные элементы структуры и структуры . Мы поэтому имеем две структуры на множестве , одна получена из структуры отображением в , а другая получена из отражением в . Консерватор выигрывает, если эти структуры одинаковы. Новатор выигрывает, если они не одинаковы.
Для любого n мы определяем отношение , если Консерватор выигрывает в игре с n ходами . Это все отношения эквивалентности на классе структур с заданными символами отношений. Пересечение всех этих отношений снова является отношением эквивалентности .
Легко доказать, что если Консерватор выигрывает игру для всех n, то есть , то и элементарно эквивалентны. Если множество отношений символов конечно, обратное тоже верно.
История
(или метод подбора), использованный в игре Эренфойхта — Фраиса для проверки элементарной эквивалентности предложил в своей диссертации. Метод сформулировал в виде игры . Названия Spoiler и Duplicator дал Joel Spencer. Также используются названия Eloise и Abelard (и обозначаются часто и ) по именам Элоиза и Абеляр, по схеме именований, предложенной в его книге Теория моделей.
Литература для дальнейшего чтения
Глава 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)
Категория:Теория моделей