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

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

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

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

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

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

Определение

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

  1. Первый игрок, Спойлер, выбирает либо члена , либо члена . а 1 {\displaystyle а_{1}} А {\displaystyle {\mathfrak {A}}} б 1 {\displaystyle b_{1}} Б {\displaystyle {\mathfrak {B}}}
  2. Если Спойлер выбрал члена , Дубликатор выбрал члена ; в противном случае Дубликатор выбрал члена . А {\displaystyle {\mathfrak {A}}} б 1 {\displaystyle b_{1}} Б {\displaystyle {\mathfrak {B}}} а 1 {\displaystyle а_{1}} А {\displaystyle {\mathfrak {A}}}
  3. Спойлер выбирает либо члена , либо члена . а 2 {\displaystyle а_{2}} А {\displaystyle {\mathfrak {A}}} б 2 {\displaystyle b_{2}} Б {\displaystyle {\mathfrak {B}}}
  4. Дубликатор выбирает элемент или модель, из которой Спойлер не выбрал. а 2 {\displaystyle а_{2}} б 2 {\displaystyle b_{2}}
  5. Спойлер и Дубликатор продолжают выбирать участников для дальнейших шагов. А {\displaystyle {\mathfrak {A}}} Б {\displaystyle {\mathfrak {B}}} н − 2 {\displaystyle n-2}
  6. В конце игры мы выбрали различные элементы из и из . Таким образом, у нас есть две структуры на множестве , одна из которых индуцирована из через карту, отправляющую в , а другая индуцирована из через карту, отправляющую в . Дубликатор побеждает, если эти структуры одинаковы; Спойлер побеждает, если они не одинаковы. а 1 , … , а н {\displaystyle a_{1},\точки ,a_{n}} А {\displaystyle {\mathfrak {A}}} б 1 , … , б н {\displaystyle b_{1},\точки ,b_{n}} Б {\displaystyle {\mathfrak {B}}} { 1 , … , н } {\displaystyle \{1,\точки,n\}} А {\displaystyle {\mathfrak {A}}} я {\displaystyle я} а я {\displaystyle a_{i}} Б {\displaystyle {\mathfrak {B}}} я {\displaystyle я} б я {\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 \существует} ∀ {\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 страницы)
Retrieved from "https://en.wikipedia.org/w/index.php?title=Ehrenfeucht–Fraïssé_game&oldid=1155140107"