Игра Эренфойхта – Фраиссе - Ehrenfeucht–Fraïssé game

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

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

Главная идея

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

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

Определение

Предположим, что нам даны две структуры ${\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}}}$; в противном случае Duplicator выберет участника ${\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}}$. Дубликатор выигрывает, если эти структуры совпадают; Спойлер побеждает, если их нет.

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

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

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

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

История

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

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

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

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

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

Рекомендации

1. Боссе, Уве (1993). «Игра Эренфойхта – Фраиссе для логики фиксированных точек и стратифицированной логики фиксированных точек» (PDF). В Börger, Egon (ред.). Логика информатики: 6-й семинар, CSL'92, Сан-Миниато, Италия, 28 сентября - 2 октября 1992 г. Избранные статьи. Конспект лекций по информатике. 702. Springer-Verlag. С. 100–114. Дои:10.1007/3-540-56992-8_8. ISBN  3-540-56992-8. Zbl  0808.03024.
2. Sur une nouvelle классификации систем отношений, Ролан Фраиссе, Comptes Rendus 230 (1950), 1022–1024.
3. Sur quelques классификации систем отношений, Ролан Фраисс, диссертация, Париж, 1953; опубликовано в Публикации Scientifiques de l'Université d'Alger, серия А 1 (1954), 35–182.
4. Приложение игр к проблеме полноты формализованных теорий, А. Эренфойхт, Fundamenta Mathematicae 49 (1961), 129–141.
5. Стэнфордская энциклопедия философии, статья о логике и играх.
6. Курс теории моделей, Bruno Poizat, tr. Моисей Кляйн, Нью-Йорк: Springer-Verlag, 2000.
7. Линейные порядки, Джозеф Г. Розенштейн, Нью-Йорк: Academic Press, 1982.
8. Пример игры Эренфойхта-Фраиссе.
9. Курс Фокиона Колайтиса по комбинаторным играм по теории конечных моделей (файл .ps)
10. Нил Иммерман (1999). "Глава 6: Игры Эренфойхта – Фраиссе". Описательная сложность. Springer. С. 91–112. ISBN  978-0-387-98600-5.

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

внешняя ссылка

• Шесть лекций по играм Эренфойхта-Фраисе в MATH EXPLORERS 'CLUB на математическом факультете Корнелла.
• Modeloids I, Мирослав Бенда, Труды Американского математического общества, Vol. 250 (июнь 1979 г.), стр. 47 - 90 (44 страницы)