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

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

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

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

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

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

Определение

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

Первый игрок, Спойлер, выбирает одного из участников. $a_{1}$ из ${\mathfrak {A}}$ или член $b_{1}$ из ${\mathfrak {B}}$ .
Если бы Спойлер выбрал члена ${\mathfrak {A}}$ , Дубликатор выбирает участника $b_{1}$ из ${\mathfrak {B}}$ ; в противном случае Duplicator выбирает участника $a_{1}$ из ${\mathfrak {A}}$ .
Спойлер выбирает любого участника $a_{2}$ из ${\mathfrak {A}}$ или член $b_{2}$ из ${\mathfrak {B}}$ .
Дубликатор выбирает элемент $a_{2}$ или $b_{2}$ в той модели из которой не выбирал Спойлер.
Спойлер и Дубликатор продолжают выбирать участников ${\mathfrak {A}}$ и ${\mathfrak {B}}$ для $n-2$ больше шагов.
В конце игры мы выбрали отдельные элементы. $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}}\ {\overset {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}}$ элементарно эквивалентны. Если набор рассматриваемых символов отношения конечен, верно и обратное.

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

История

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

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

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

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

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

Ссылки

^ Боссе, Уве (1993). «Игра Эренфойхта – Фрессе для логики с фиксированной точкой и стратифицированной логики с фиксированной точкой» (PDF) . В Бёргере, Эгон (ред.). Логика информатики: 6-й семинар, CSL'92, Сан-Миниато, Италия, 28 сентября - 2 октября 1992 г. Избранные статьи . Конспекты лекций по информатике. Том. 702. Шпрингер-Верлаг . стр. 100–114. дои : 10.1007/3-540-56992-8_8 . ISBN 3-540-56992-8 . Збл 0808.03024 .
^ О новой классификации систем отношений , Ролан Фрейссе, Comptes Rendus 230 (1950), 1022–1024.
^ О некоторых классификациях систем отношений , Ролан Фрэссе, диссертация, Париж, 1953;опубликовано в «Научных публикациях Алжирского университета» , серия А 1 (1954), 35–182.
^ Приложение игр к проблеме полноты формализованных теорий , А. Эренфойхт, Fundamenta Mathematicae 49 (1961), 129–141.
^ Стэнфордская энциклопедия философии, статья о логике и играх.
^ Курс теории моделей , Бруно Пуаза, тр. Мозес Кляйн, Нью-Йорк: Спрингер-Верлаг, 2000.
^ Линейные порядки , Джозеф Г. Розенштейн, Нью-Йорк: Academic Press, 1982.
^ Пример игры Эренфойхта-Фрессе.
^ Курс комбинаторных игр в теории конечных моделей Фокиона Колайтиса (файл .ps)
^ Нил Иммерман (1999). «Глава 6: Игры Эренфойхта – Фрэссе» . Описательная сложность . Спрингер. стр. 91–112. ISBN 978-0-387-98600-5 .

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

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

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

[1] Боссе, Уве (1993). «Игра Эренфойхта – Фрессе для логики с фиксированной точкой и стратифицированной логики с фиксированной точкой» (PDF) . В Бёргере, Эгон (ред.). Логика информатики: 6-й семинар, CSL'92, Сан-Миниато, Италия, 28 сентября - 2 октября 1992 г. Избранные статьи . Конспекты лекций по информатике. Том. 702. Шпрингер-Верлаг . стр. 100–114. дои : 10.1007/3-540-56992-8_8 . ISBN 3-540-56992-8 . Збл 0808.03024 .

[2] О новой классификации систем отношений , Ролан Фрейссе, Comptes Rendus 230 (1950), 1022–1024.

[3] О некоторых классификациях систем отношений , Ролан Фрэссе, диссертация, Париж, 1953;опубликовано в «Научных публикациях Алжирского университета» , серия А 1 (1954), 35–182.

[4] Приложение игр к проблеме полноты формализованных теорий , А. Эренфойхт, Fundamenta Mathematicae 49 (1961), 129–141.

[5] Стэнфордская энциклопедия философии, статья о логике и играх.

[6] Курс теории моделей , Бруно Пуаза, тр. Мозес Кляйн, Нью-Йорк: Спрингер-Верлаг, 2000.

[7] Линейные порядки , Джозеф Г. Розенштейн, Нью-Йорк: Academic Press, 1982.

[8] Пример игры Эренфойхта-Фрессе.

[9] Курс комбинаторных игр в теории конечных моделей Фокиона Колайтиса (файл .ps)

[Immerman1999-10] Нил Иммерман (1999). «Глава 6: Игры Эренфойхта – Фрэссе» . Описательная сложность . Спрингер. стр. 91–112. ISBN 978-0-387-98600-5 .

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]