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

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

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

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

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

Игра длится фиксированное количество шагов (которое является порядковым числом — обычно конечным числом или ). ${\displaystyle \gamma }$ ${\displaystyle \omega }$

Определение

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

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

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

Эквивалентность и невыразимость

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

Если свойство верно для , но не верно для , но и может быть показано эквивалентным, предоставив выигрышную стратегию для Duplicator, то это показывает, что оно невыразимо в логике, запечатленной в этой игре. ^{[ необходимо дальнейшее объяснение ]} ${\displaystyle Q}$ ${\displaystyle {\mathfrak {A}}}$ ${\displaystyle {\mathfrak {B}}}$ ${\displaystyle {\mathfrak {A}}}$ ${\displaystyle {\mathfrak {B}}}$ ${\displaystyle Q}$

История

Метод «туда-сюда», используемый в игре Эренфойхта–Фрайсса для проверки элементарной эквивалентности, был предложен Роланом Фрайссом в его диссертации; ^{[2] [3]} он был сформулирован как игра Анджеем Эренфойхтом . ^[4] Названия Спойлер и Дубликатор принадлежат Джоэлу Спенсеру . ^[5] Другие обычные названия — Элоиза [sic] и Абеляр (и часто обозначаются и ) в честь Элоизы и Абеляра , схемы именования, введенной Уилфридом Ходжесом в его книге «Теория моделей» , или, альтернативно, Евы и Адама. ${\displaystyle \exists }$ ${\displaystyle \forall }$

Дальнейшее чтение

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

На слайдах Фокиона Колайтиса ^[9] и в главе книги Нила Иммермана ^[10] об играх Эренфойхта–Фрайсса обсуждаются приложения в информатике, методология доказательства результатов невыразимости и несколько простых доказательств невыразимости с использованием этой методологии.

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

Ссылки

1. Bosse, Uwe (1993). "Игра Эренфойхта–Фрайсса для логики с фиксированной точкой и стратифицированной логики с фиксированной точкой" (PDF) . В Börger, Egon (ред.). Computer Science Logic: 6th Workshop, CSL'92, San Miniato, Italy, September 28 - October 2, 1992. Selected Papers . Lecture Notes in Computer Science. Vol. 702. Springer-Verlag . pp. 100–114. doi :10.1007/3-540-56992-8_8. ISBN 3-540-56992-8. Збл  0808.03024.
2. Sur une nouvelle классификация систем отношений , Ролан Фрэссе, Comptes Rendus 230 (1950), 1022–1024.
3. Sur Quelques Classifications des Systemes de Relations , Ролан Фрэссе, диссертация, Париж, 1953; опубликовано в Publications Scientifiques de l'Université d'Alger , серия A 1 (1954), 35–182.
4. Применение игр к проблеме полноты формализованных теорий, А. Эренфойхт, Fundamenta Mathematicae 49 (1961), 129–141.
5. Стэнфордская энциклопедия философии, статья о логике и играх.
6. Курс теории моделей , Бруно Пуаза, пер. Мозеса Кляйна, Нью-Йорк: Springer-Verlag, 2000.
7. Линейные порядки , Джозеф Г. Розенштейн, Нью-Йорк: Academic Press, 1982.
8. Пример игры Эренфойхта-Фрессе.
9. Курс по комбинаторным играм в теории конечных моделей Фокиона Колайтиса (файл .ps)
10. Нил Иммерман (1999). «Глава 6: Игры Эренфойхта – Фрэссе». Описательная сложность . Спрингер. стр. 91–112. ISBN 978-0-387-98600-5.

• Грэдель, Эрих; Колайтис, Фокион Г.; Либкин, Леонид; Маартен, Маркс; Спенсер, Джоэл ; Варди, Моше Й .; Венема, Иде; Вайнштейн, Скотт (2007). Теория конечных моделей и ее приложения . Тексты по теоретической информатике. Серия EATCS. ​​Берлин: Springer-Verlag . ISBN 978-3-540-00428-8. Збл  1133.03001.

Внешние ссылки

• Шесть лекций по играм Эренфойхта-Фрайсса в КЛУБЕ МАТЕМАТИЧЕСКИХ ИССЛЕДОВАТЕЛЕЙ, кафедра математики Корнеллского университета.
• Modeloids I, Мирослав Бенда, Труды Американского математического общества, т. 250 (июнь 1979 г.), стр. 47–90 (44 страницы)