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

Связи между логикой и играми уходят в историю. Если рассматривать дебаты в качестве игры, то уже  Аристотель создал эту связь; его писания о силлогизме были тесно связаны с учением о целях и правилах дебатов. Взгляды Аристотеля сохранились в близком для логики средневековом названии: диалектике. В середине двадцатого века Чарльз Хамблин возобновил связь между диалектикой и правилами здравого смысла. Немного позже Пол Лоренц соединил диалектику с конструктивными основами логики.

Существуют тесные связи между играми и учебой. Писатели средневекового периода рассматривают диалог в ключе «обучения» и «тестирования» пользы здравого смысла.

Существует как минимум две книги о логике из ранних шестидесятых, которые позиционируют ее как игру для индивидуального студента, и в книге Льюса Кэррола «Игра логики» (1887) есть более ранние пример этого рода.

Математическая теория игр была основана в начале двадцатого века. Но никаких связей с логикой не возникло  до 1950-ых годов. Поразительно, что многие из пионеров теории игр также известны трудами в области логики: John Kemeny, J. C. C. McKinsey, John von Neumann, Willard Quine, Julia Robinson, Ernst Zermelo и др. В 1953 году Дэвид Гейл и Фрэнк Стюарт установили плодородную связь между теорией множеств и играми. Вскоре, Леон Хенкин предложил вариант использования игр для получения семантики бесконечных языков.

Первая половина двадцатого века была эрой роста точности и профессионализма в логике, и для большинства логиков этого периода использование игр, вероятно, могло казаться фривольностью. Интуит  Броуэр выражал именное такое свое отношение, когда обвинял своих оппонентов в том, что их действия «вырождают математику в игру» (как Дэвид Гильбетр цитировал его в 1927). Герман Вэйл использовал понятие игры для объяснение математики Гильберта: математические доказательства развиваются как ходы в бессмысленной игре, но мы может стоять в стороне от игры и задать бессмысленные вопросы о ней. Языковые игры  Виттенгштейна спровоцировали слабый резонанс со стороны логиков. Но во второй половине века центр тяжести исследований логики сместился от фундаментальности к технике, и с 1960-ых игры использовались все чаще и чаще в их работах.

2.       Логические игры.

С точки зрения теории игр, игры, возникшие в логике, не являются типичными. Они обычно включают только двух игроков, и часто имеют бесконечную длину. Исходом служит лишь выигрыш или поражение, и никакие вероятности не связаны с действиями внутри игры и ее результатами. Лишь малая часть основных логических игр схожи с нижеописанными.

Есть два игрока. Без ограничения общности мы можем называть их А и Е. Произношения Абелард и Элоиза относятся к середине 1980-ых и фиксируют игроков как мужчину и женщину (так как логики-феминисты требовали подходящего выбора и этого параметра).  Другие имена совместно используются для игроков в конкретных типах логических игр.

Игроки играют, выбирая элементы множества О, называемого областью определения игры. С выбором выстраивается последовательность:

А1,а2, а3, ...

Элементов из О. Бесконечные последовательности элементов из О называются игрой. Конечные послеовательности элементов из О называются позициями; они записывают то, где игра может находиться, спустя некоторое время. Функция Тау (фукнция игрока)присваивает  каждую позицию А или Е; если .... τ(a) = Е означает, что когда игра достигнет а, игрок Е сделает следующий выбор (аналогично и игрок А). Правила игры определяют два множества W_∀ и W_∃, состоящие из позиций и игр со следующими свойствами: если позиция

a лежит в W_∀, то также в ней лежит и любая игра или позиция, начинающаяся с а и длиннее ее (и аналогично с W_∃); ни одна позиция не находится сразу в W_∀ и W_∃. Будем говорить, что игрок ∀ выигрывает игру b, и b является победной для ∀, если b лежит в W_∀; если какая-то позиция а, являющаяся частью b, лежит в W_∀, то будем говорить, что игрок ∀ выигрывает уже наa. (и аналогично с ∃ и W_∃.) Таким обраом, логическая игра состоит из четырех элементов (Ω, τ, W_∀, W_∃) со свойствами, описанными выше.

Будем говорить, что логическая игра полна, если любая игра лежит в W_∀ или W_∃, так что нет ничьих. Пока не будет сделано исключение, полагаем все логические игры полными. (Не следует путать понятия быть полной и быть детерминированной – смотри ниже.)

В определении, описанной выше, только для математической строгости игра должна продолжаться бесконечно, даже если игрок выиграл в конечной позиции; на самом деле нет интереса ни в чем, произошедшем после того, как игрок победил. Многие логические игры обладают тем свойством, что в каждой игре они из игроков уже победил на какой-либо конечной позиции; игры такого типа называют обоснованными. Более сильным является условие, что к какому-либо конечному шагу n каждой игры один из игроков уже победил; в таком случае игры имеют конечную длину.

Стратегия игрока – множество правил, описывающих в точности, какой игроку следует сделать выбор, основываясь на том, как оба игрока выбирали предыдущие шаги. Гвооря строго, стратегия для А состоит из функции, которая выбирает для любой позиции а с тау(а) = А элемент b из О; будем рассматривать это как инструкцию для А выбирать b, когда игра достигла позиции а. (Аналогично для стратегии игрока Е.) Стратегию игрока назовем выигрышной, если этот игрок выигрывает любую игру, в которой он использует стратегию, не зависимо от действий другого игрока. Максимум один игрок может обладать выигрышной стратегией (если оба обладают выигрышными стратегиями, то они оба выиграют, противореча тому, что W_∀ и W_∃ не имеют общих элементов). Возможно возникновении ситуаций, в которой кажется, что оба игрока имеют выигрышную стратегию (например, в силовых играх, описанных ниже), но ближайшее рассмотрение показывает, что, на самом деле, оба игрока играют в разные игры.

Назовем игру детерминированной, если один или несколько игроков имеют выигрышную стратегию. Существует много примеров недетерминированных игр, как показали Гейл и Стюарт в 1953 г., используя аксиому выбора. Это открытие привело к важному приложению понятия детерминированности в основах теории множеств. Гейл и Стюарт также доказали важную теорему, носящую их имена, утверждающую: Каждая убедительная игра детерминирована. Отсюда вытекает, что каждая конечная игра детерминирована – факт, уже известный Зермело в 1913 г.(Более точное утверждение теоремы Гейла-Стюарта таково: Игра G называется закрытой, если Е выигрывает каждую партию G, в которой она не проиграла ни на какой конечной позиции. Теорема утверждает, что каждая закрытая игра детерминирована.)

Как и в классической теории игр, определение логической игры, описанное выше, выступает в качестве одежки, которую мы можем накинуть на другую концепцию. Например, принято иметь несколько правил, описывающих те элементы из Ω, которые доступны игроку при выборе конкретного хода. Данное условие не необходимо, так как выигрышные стратегии не изменятся, если мы установим правило, что игрок, нарушающий правило, проигрывает мгновенно; но для многих игр такой взгляд кажется неестественным. Ниже мы увидим некоторые другие особенности, которые могут быть добавлены к играм.

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

Коротко, игры используются для моделирования рационального и ограниченного рационального поведения. Это не зависит от какой-либо связи с логикой. Но некоторые логики были построены для изучения аспектов рационального поведения, и в последние годы особенно, стало принято связывать логику с подходящими играми. См. Раздел 4 «Больше семантических игр и их библиография».

Но до недавнего времени логические игры были связаны с рациональным поведением немного другим образом. На первый взгляд, логика не имеет прямой связи с поведением. Но логики и математики отмечали, что некоторые идеи могли бы быть более понятны интуитивно, если бы были связаны с возможными целями в играх. Например, во многих приложениях логических игр главным понятием  являлась победная  стратегия для игрока Е. Обычно эти стратегии (или их существование) оказывались эквивалентными чему-то важному с логической точки зрения, и что могло бы быть определено без использования игр – например, доказательство. Но игры были бессильны в предложении этим объектам определений, поскольку в них достаточно буквально поддерживалась некоторая мотивация: Е пытается выиграть.

Это подняло вопрос не столь интересный для математиков, но, безусловно, заинтересовавший философов, использующих логические игры. Если мы хотим оценить мотивацию игрока Е в игре G некоторым значением, то нам необходимо понимать, что является достижением, если игрок Е выигрывает. В частности, нам нужно иметь возможность рассказать реалистичную историю о ситуации, в которой некоторый агент, именуемый Е, пытается сделать что-либо осмысленное, и процесс совершения этих действий есть то же, что победа в игре. Как говорил Ричард Доскины, поднимая соответствующий вопрос для эволюционных игр Мэйнарда Смитта,

«Вся цель поиска ... это открытие подходящего актера, играющего ведущую роль в наших метафорах цели. Мы ... хотим сказать: «Это - для блага ...». Наша цель в этом разделе – найти правильное окончание этой фразы.

В будущих ссылках будем называть это вопросом Доукинса. Во многих видах логической игры  ответить на вопросы оказывается значительно труднее, чем представляли себе основатели.

3.     Семантические игры.

В начале 1930-ых Альфред Тарский предложил определение истины. Его определение состояло из необходимого и достаточного условия истинности для высказывания, написанного на языке обычной формальной теории; его необходимые и достаточные условия использовали только понятия синтаксиса и теории множеств, вместе с примитивными понятиями формальной теории в вопросе. На самом деле Тарский определил более общую связь ‘формула φ(x₁,…, x_n) истинна на элементах a₁,…, a_n’; истинность высказывания - специальный случай при n = 0. Например, вопрос о том, является ли

‘Для каждого x существует y такой, что R(x, y)’ истинным, возвращает нас к вопросу о том, имеет ли место следующее:

Для любого объекта a высказывание ‘Существует такой y, что R(a, y)’ истинно.

Это, в свою очередь, ведет к следующему:

Для любого объекта a существует объект b такой, что высказывание ‘R(a, b)’ истинно.

Данный пример построен на определении истинности Тарского.

В конце 1950-ых Леон Хенкин отметил, что мы можем интуитивно понять некоторые высказывания, которые не могут быть идентифицированы в определении Тарского. Возьмем, для примера, бесконечно длинное высказывание:

Для всех x₀ существует y₀ такой, что для всех x₁ существует y₁ такой, что  … R(x₀, y₀, x₁, y₁,…).

Подход Тарского проваливается потому, что последовательность квантеров в начале – бесконечна, и мы никогда не достигнем конца, раскручивая их таким образом. Вместе этого Хенкин предложил нам рассмотреть игру, где игрок ∀ выбирает объект a₀ для x₀,затем второй игрок ∃ выбирает объект b₀ для y₀, потом ∀ выбирает a₁ для x₁, ∃ выбирает b₁ для y₁ и так далее. Партия в этой игре выигрышна для ∃ тогда, и только тогда, когда бесконечное атомарное высказывание

R(a₀, b₀, a₁, b₁,…)

 истинно.  Исходное высказывание истинно тогда, и только тогда, когда игрок Е обладает выигрышной стратегией для данной игры.  Определенно, Хенкин использовал игру только как метафору, и условие истинности, предложенное им, являлось лишь сколемизированной версией истинности высказывания, то есть что существуют функции f₀, f₁, … такие, что для любого выбораa₀, a₁, a₂ и т.д. имеется

R(a₀, f₀ (a₀), a₁, f₁ (a₀, a₁), a₂, f₂(a₀, a₁, a ₂), …).

Но это условие моментально переводится на язык игр; функции Сколема  f₀ и т.д..определяют выигрышную стратегию для ∃, рассказывая ей, как поступать в свете предыдущих ходов, сделанных ∀. (Эти идеи увидели свет несколько позже предложения Ц.С.Пирса, объясняющего разницу между «каждым» и «несколькими» в терминах тех, кто выбирает объект; идеи были предложены в его лекции второй кембриджской конференции 1898.)

Вскоре после работы Хенкина, Яакко Хинтикка отметил факт, что подобная идея применима к конъюнкциям и дизъюнкциям. Мы можем рассматривать конъюнкцию ‘φ ∧ ψ’ как универсальное определенное высказывание означающее ‘Имеет место каждое из высказываний φ, ψ’, поэтому игроку ∀ следует выбрать одно из высказываний. Во введенных Хинтиккой понятиях, при игре G(φ∧ψ), ∀ выбирает то, как продолжится игра: как G(φ) или как G(ψ). Аналогично и дизъюнкции становятся экзистенционально измеримыми утверждениями о множествах высказываний, и они отмечают ходы, в которых игрок ∃ выбирает, как будет продолжаться игра. Для приведения кванторов, он предложил, чтобы игра G(∀ x φ(x)) продолжалась следующим образом: игрок ∀ выбирает объект и называет его a, и игра продолжается как G(φ(a)). (Аналогично и с экзистенциональными кванторами, кроме тех, что выбирает Е). Хинтакка также внес искусное предложение для представления отрицания. Каждая игра G имеет двойственную игру, которая совпадает с G, кроме того момента, что ∀ и ∃ поменяны местами во всех правилах проведения игры и определении победы. Игра G(¬φ) двойственна G(φ).

Можно доказать, что для любого высказывания первого порядка, описанного в фиксированной структуре А, игрок Е обладает выигрышной стратегией для игры Хинтакки G(φ) тогда, и только тогда, когда φ истинной в A в смысле Тарского. Интересны два момента данного доказательства. Во-первых, если φ является высказыванием первого порядка, то игра G(φ) имеет конечную длину, и поэтому теорема Гейла-Стюарта утверждает, что она детерминирована. Мы утверждаем, что ∃ обладает выигрышной стратегией ровно в одной из G(φ) и двойственной к ней; поэтому, у нее есть выигрышная стратегия в G(¬φ) тогда, и только тогда, когда у нее ее нет в G(φ). Это решает вопрос отрицания. Следует обратить внимание на еще один момент: если ∃ обладает выигрышной стратегией для каждой игры G(φ(a)), то после выбора одной такой стратегии f_a для каждого a, она может соединить их вместе в единую выигрышную стратегию для G(∀x φ(x)) (дословно, ‘Жди и смотри, какую стратегию a выберет ∀, затем играй f_a’). Это решает ситуацию с универсальными кванторами; но аргумент использует аксиому выбора, и на самом деле несложно видеть, что эквивалентность определений истины Хинтакки и Тарского в свою очередь эквивалентна аксиоме выбора (построенной из других аксиом теории множеств Зермело-Фрэнкела).

Интересно, что у нас есть две теории истинности высказываний, и они не эквивалентны, если аксиома истинности не верна. На самом деле, причина не столь глубока. Аксиома выбора необходима не потому, что определение Хинтакки использует игры, а потому, что предполагается, что стратегии детерминированы. Таким образом, они являются однозначными функциями, не дающим пользователю право выбора. Более естественный способ перевода определения Тарского в термины игр – это использование недетерминированных стратегий (Хотя, Хинтакка в 1996 настоял на том, что корректным пояснением понятия «истина» является то, которое использует детерминированные стратегии, и этот факт доказывает аксиому выбора.)

Компьютерные применения этих игр Хинтакки оказались высоко эффективными в обучении значений высказываний первого порядка. Один подобный пакет был спроектирован Джоном Борвайзос и Джоном Этчеменди в Стэнфорде и называется  «Мир Тарского». Независимо от них другая команда университета из Омска создала русскую версию для школ, обучающих одаренных детей.

В опубликованной версии его лекций в Оксфорде 1973 года, Хинтакка поднимает вопрос Доукинса (смотри выше) об этих играх. Его ответ заключался в том, что следует обратиться к языковым играм Виттгенштайна, и языковые игры для понимания кванторов являются как раз теми, которые как раз и вращаются вокруг поиска и нахождения ответа. В соответствующих играх можно рассмотреть Е как самого себя, и А как враждебно настроенную Природу, на которую нельзя опереться в контексте представления объекта, который мне нужен. Таким образом, для уверенности ее нахождения , мне необходима выигрышная стратегия. Эта история никогда не была достаточно убедительной. Мотивация Природы нерелевантная, и ничто в логической игре не соотносится с поиском. Взгляд в прошлое приносит небольшое разочарование оттого, что никто не озадачивался проблемой поиска лучшей истории. Более полезным мог быть подход рассмотрения выигрышной стратегии для ∃ в G(φ) как некоторого вида доказательства (в подходящей бесконечной системе) такого, что φ истинно.

Позже Яакко Хинтакка расширил идеи в двух направлениях, а именно естественной языковой семантике и играх с неидеальной информацией (смотри следующий раздел). Название «Игро-Теоретическая семантика», коротко ИТС, появилось для покрытия обоих направлений.

Игры, описанные в этом разделе, почти тривиально адаптируются к многозначной логике. Например, квантор ∀x, где x переменная типа σ, является инструкцией для игрока ∀ выбрать элемент типа σ. Это сразу дает нам соответствующие игры для логики второго порядка, если мы рассматриваем элементы структуры в качестве первого типа, множества элементов как второй тип, бинарные отношения - как третий и т.д. Отсюда следует, что у нас есть правила игр также и для более общих кванторов; их мы можем найти, если сначала переведем эти кванторы в логику второго порядка.

4.     Больше семантических игр.

Структуры подобного типа приводят к интересным играм. Структура A состоит из множества S элементов (которые мы назовем состояниями, но часто они называются мирами), бинарное отношения R на S (нам следует читать как R  стрелка), и семейство подмножеств P₁,…, P_n множества S. Два игрока ∀ и ∃ играют в игру G на A (начиная с состояния s, которое дается им) путем чтения подходящей логической формулы φ в качестве множества инструкция для игры и победы в ней.

Таким образом, если φ это P_i, то игрок ∃ выигрывает сразу, если  s лежит в P_i, в противном случае сразу выигрывает ∀. Формулы ψ∧θ, ψ∨θ и ¬ψ описывают то же поведение, что и в играх Хинтакки. Например, ψ∧θ инструктирует игрока ∀ выбирать такую стратегию, чтобы игра продолжилась для ψ или θ. Если формулы φ  □ψ, то игрок ∀ выбирает стрелку из s в состояние t (таким образом, состояние t такого, что пара (s, t) лежит в отношении R). Игра затем продолжается из состояния t по инструкциям ψ. Правило для ◊ψ такое же, кроме того, что выбор принимает игрок ∃. Наконец, назовем формулу φ истинной на s в  A если игрок ∃ обладает выигрышной стратегией для этой базовой игры на φ с началом в s.

Эти игры относятся к модальной логике тем же образом, как и игры Хинтакки к логике первого порядка. В частности, они придерживаются одного из путей привнесения семантики в модальную логику, а также согласованы с обычной семантикой Крипке-типа. Безусловно, есть много типов и обобщений модальной логики (включая такие тесно связанные логики, как временная логика, эпистемика и динамическая логика.), и соответствующие игры проявляются в различных формах. Одним из интересных примеров является компьтерно-теоретическая логика Мэттью Хеннеси и Робина Милнера., используемая для описания систем; в ней стрелки бывают более, чем одного цвета, и движение по стрелке конкретного цвета представляет конкретное действие, изменяющее состояние. Другим примером является более сильное модальное μ-исчисление Дэкстера Козена, которое зафиксировало точечные операторы; смотри главу 5 Стирлинга (2001).

В схожей «логике игр», предложенной Рохитом Парихом, игры, перемещающие нас между состояниями, являются предметом изучения больше, чем способ получения определения истинности. У этих игр есть много интересных особенностей. В 2003 г. В журнале Studia Logica была тема, посвященная именно им, написанная Марком Паули и Парихом.

Возможны различные типы корректировок семантических игр для отбрасывания предположения о том, что игроки знают предыдущую историю игры. Например, мы может потребовать от игрока делать выбор без информации о том, какое решение принял другой игрок на предыдущих шагах. Классический способ достижения подобного результата - это создание ограничений на стратегии игроков. Например, можно потребовать, чтобы функция стратегии, говорящая Е, что делать на данной конкретном шаге, являлась функцией с областью определения, являющимся семейством возможных ходов для игрока А на его первом и втором шагах. Это – путь описания ситуации, когда Е не знает, какие решения принимал А на 3-ем и последующих шагах. Игры с ограничениями подобного рода на функции стратегий принято называть играми с неидеальной информацией, в противопоставление играм с идеальной информацией, описанным в предыдущей главе.

Классическим примером логики с семантической игрой с неидеальной информацией является Независимость-Дружба логика Хинтакки и Габриэля Санду. Эта логика такая же, что и логика первого порядка с игро-теоретической семантикой Хинтакки, кроме корректировки понятий некоторых кванторов (и, возможно, некоторых связей), для выявления того, что функции Сколема для этих кванторов (или соединений) независимы от конкретных переменных. Например, высказывание

(∀x)(∃y/ ∀x)R( x, y)

читается, как «Для любого x существует y, не зависящий от x, такой, что R(x, y)»

Следует прокомментировать три важных отличия между идеальной и неидеальной информацией. Во-первых, теорема Гейла-Стюарта имеет место только для игр с идеальной информацией. Положим, для примера, что ∀ и ∃ играют в следующую игру. Сначала А выбирает число 0 или 1. Затем Е – одно из этих чисел. Игрок Е выигрывает, если оба числа одинаковы, а в противном случае победу одерживает игрок А. Нам необходимо, чтобы Е в момент принятия решения не знала о выборе А, поэтому функции Сколема для нее будут константой. Эта игра соответствует НД высказыванию, описанному выше, где R – равенство, а структура множества определения состоит из 0 и 1. Понятно, что у игрока Е нет выигрышной стратегии, и также ею не обладает игрок А. Эта игра – недетерминирована, хотя ее длина равна всего лишь 2.

Одним из следствий является то, что обоснование Хинтакки рассмотрения отрицания как дуализма (игроки меняются местами) в его играх для логик первого порядка не распространяется на НД логику. Хинтакка утверждал, что дуализм является корректным интуитивным значением отрицания даже в случае логики первого порядка, поэтому никакого обоснования не нужно.

Вторым замечанием является то, что даже в играх с идеальной информацией может случиться так, что выигрышные стратегии не используют всю доступную информацию. Например, в игре с идеальной информацией, если игрок Е обладает выигрышной стратегией, то она также обладает выигрышной стратегией, в которой функции стратегии зависят только от последнего хода игрока А (Это происходит потому, что она может перестроить свое собственные ходы, используя предыдущие функции стратегии). Более оригинальным случаем являются модальные игры, описанные выше: игроку для перехода из состояния s не надо знать, как он или она достигли этого состояния, поэтому предыдущая история игры не важна. Как выражаются компьютерщики, это – игры «без памяти».

Когда Хинтакка использовал функции сколема в играх логики первого порядка, он строил стратегии для игрока зависящими только от предыдущих ходов другого игрока. Функция сколема для игрока Е зависит только от универсальных квантифицированных переменных.

Ввиду того, что рассмотренные игры являлись играми с идеальной информацией, второй комментарий не создает проблем. Но если двигаться в направлении НД логики, возникает следующее требование к стратегиям: они должны зависеть только от тех ходов другого игрока, которые действительно были важны. Ходжс показал это путем пересмотра понятий таким образом, что, например, (∃y/x) означает: существует y, не зависящий от x, не зависящий также от того, какой игрок выбрал x.

Теперь рассмотрим высказывание:

(∀x)(∃z)(∃y/ x)( x=y),

построенное на структуре элементов, состоящей из 0 и 1. Игрок Е может выиграть в нижеописанном случае. Для z она делает тот же выбор, что и А при выборе x; затем, для y он выбирает ту же стратегию, что и для z. Выигрышная стратегия работает только потому, что в этой игре Е может ссылаться на свои ранее принятые решения. У нее не было бы выигрышной стратегии, если бы третьим квантором был (∃y/xz), опять же потому, что функция сколема для этого квантора должна была бы константой. Тот путь, с помощью которого Е передает информацию себе о своих же предыдущих ходах, является примером феномена сигнализирования. Джон фон Нейман и Оскар Моргенстерн проиллюстрировали это на примере брижда, где каждый «игрок» состоит из двух партнеров, которые должны делиться информацией, используя публично сигналы друг другу.

Третий момент заключается в том, что здесь имеет место дислокация между интуитивной идеей неидеальной информации и его теоретическо-игровым определением в терминах стратегий. Интуитивно рассуждая, неидеальная информация является результатом обстоятельств, в которых проходит игра, но никак не стратегии. Это очень тонкая разница, и она приводит к недопониманию при работе с НД и аналогичными логиками. Рассмотрим, например, высказывание:

 (∃x)(∃y/ x)( x=y),

Опять же на структуре элементов 0 и 1. Интуитивно можно предположить, что, если Е не разрешено запоминать на втором шаге квантор, который она выбирает на первом шаге, то маловероятно, что у нее есть выигрышная стратегия. Но на самом деле у нее она есть: «Всегда выбирай 0!».

Влияния экономики и компьютерных наук привело многих логиков к использования логики для анализа процесса принятия решения в условиях частичного незнания. Существует несколько путей представления состояний информированности. Один из них заключается том, чтобы рассмотреть их в качестве состояний миров в типе модальной структуры, которая была упомянута в начале раздела. Второй заключается в использовании НД логики или какой-либо ее вариации. Как же связаны эти приближения? Йохан ван Бентем в 2006 г.  Предоставил некоторые свои замечания и результаты по поводу этого очень естественного вопроса.

5.     Back-and-Forth Games

В 1930 г. Альфред Тарский сформулировал понятия для двух структур А и B являться элементарно эквивалентными: абсолютно одинаковые высказывания логики первого порядка, являющиеся истинными  А, являются истинными и в B. На конференции в Принстоне в 1946г. он описал это понятие, и выразил надежду, что возникнет возможность развить теорию этого понятия, которая будет «настолько же глубока, как понятие изоморфизма и другие, используемые сейчас».

(Hourya Sinaceur ed., “Address at the Princeton University Bicentennial Conference on Problems of Mathematics (December 17-19, 1946), by Alfred Tarski”, Bulletin of Symbolic Logic 6 (2000): 1-44)

Одним из естественных частей этой теории является чисто структурная необходимость и достаточность выполнения условия для двух структур являться элементарно эквивалентными. Роланд Фрайсе, француз-алжирец, был первым, кто нашел практичное условие необходимости и достаточности. Оно было открыто еще раз несколькими годами позже казахским логиком Таймановым, и переформулировано в терминах игр польского логика Andrzej Ehrenfeucht. Игры эти теперь известны как игры Ehrenfeucht-Fraïssé, или (как их иногда называют)  назад-вперед игры. Оказалось, что идея этих игр является одной из наиболее универсальных в логике двадцатого века. Они плодотворно применяются в широком круге логик и структур.

В назад-вперед играх есть две структуры А и B, и два игрока, которых принято называть Спойлер и Дупликатор (имена придуманы Джо Спенсером в ранних 1990-ых. Ранее Нейл Имменман предлагал имена Самсона и Делиха, используя соответствующие инициалы; это ставит  Спойлера на место игрока-мужчины А, и Дупликатора на место женщины Е.) Каждый шаг игры состоит из хода Спойлера, за которым следует ход Дупликатора. Спойлер выбирает элемент одной структуры, а Дупликатор должен выбрать элемент другой. После n шагов получаем две последовательности: одна - из формы А, другая – из B:

 (a₀,…, a_n-1;b ₀,…, b_n-1).

Эта позиция выигрышная для Спойлера тогда, и только тогда, когда какая-нибудь атомарная формула (одна из форм ‘R(v₀,…, v_k-1)’ или ‘F(v₀,…, v_k-1) = v_k’, или ‘v₀=v₁’, или одна из этих различных переменных) удовлетворяет следующему: или она истинна на (a₀,…, a_n-1) в A, но не на (b₀,…, b_n-1) в B, или наоборот. Условие победы Дупликатов различно в разных формах игры. В простом случае, EF(A, B), игра является выигрышной для Дупликатора тогда, и только тогда, когда начальная часть ее не является выигрышной для Спойлера (т.е. она выигрывает, если не проиграет к какому-то конечному шагу). Для каждого натурального m существует игра EF_m(A, B); в ней Дупликатор побеждает  после m шагов, если еще не проиграл к этому моменту. Все эти игры детерминированы по теореме Гейла-Стюарта. Две структуры A и B называются назад-вперед эквивалентными, если Дупликатор обладает победной стратегией для EF(A, B), и m-эквивалентными, если она обладает выигрышной стратегией для игры EF_m(A, B).

Можно доказать, что, если А и B m-эквивалентны для любого натурального m, то они элементарно эквивалентны. С другой стороны победная стратегия для Спойлера в игре EF_m(A, B) может быть трансформирована в высказывание первого порядка, которое истинно только на А или B, и в котором вложение quantifier scopes имеет не более m уровней. Таким образом, у нас есть необходимое и достаточное условие элементарной эквивалентности, и кое-что еще.

Если А и B эквивалентны, то они элементарно эквивалентны; но в назад-вперед играх эквивалентность оказывается тем же самым, что и элементарная эквивалентность в конечных логических играх, которая является более выразительная, чем логика первого порядка. Есть много вариаций игр, которые дают другие типы эквивалентностей. Например, Barwise, Immerman и Bruno Poizat независимо друг от друга описали игру, в которой два игрока обладают ровно по p пронумерованных камней; каждый игрок должен отметить свой ход выбором камня, и два хода на одном шаге игры должны быть отмечены с помощью камней, имеющих одинаковые номера. В течение игры у игроков закончатся камни, и ими будут использовать их повторно. Условие победы позиции (и всех подпозиций) для Спойлера такое же, как и раньше, кроме того, что только отмеченные к данному моменту элементы используются при оценке позиции. Существование победной стратегии для Дупликатора в этой игре означает, что две структуры согласованы с высказываниями, которые используют не более p переменных (разрешено использование переменных любое количество раз).

Теория назад-вперед игр использует совсем немного предположений о структуре логики вопроса. В результате, эти игры являются одним из немногих модельно-технических средств, которые применимы как на конечных структурах, так и на бесконечных. Это делает их одним их краеугольных камней в теоретической компьютерной науке. Описанная теория применима для измерения выразительной силы формальных языков, например, языков баз данных. Классическим результатом может, например, являться то, что конкретный язык не может различить понятия «четный» и «нечетный». Мы можем доказать это путем поиска для каждого элемента уровня n сложности формул языка пары конечных структур, для которых Дупликатор обладает победной стратегией в назад-вперед играх уровня n, но одна из структур будет обладать четным числом элементов, а вторая – нечетным. В семантике естественных языков назад-вперед игры применимы для сравнения expressive powers кванторов.

Есть также тип назад-вперед игр, которые соответствуют модальной семантике, описанной выше, в том же ключе, что и игры Ehrenfeucht-Fraïssé соответствуют игровой семантике для логики первого порядка Хинтакки. Игроки начинают игру из состояния s в структуре А и t – в структуре B. Спойлер и Дупликатор противопоставлены друг другу больше, чем ранее. Каждый раз, когда Спойлер делает ход, он выбирает движение или в А, или в B, и тогда Дупликатор должен двигаться в той же структуре. Движение всегда должно быть по направлению стрелки из данного состояния. Если между ними два игрока пошли состояния s’ в A и состояние t’ в B, и какой-либо предикат Pi имеет место только на s’ или t’, то Дупликатор тут же проигрывает. Если два игрока играют в игру с начальными состояниями s в A и t в B, и обе структуры конечны, то можно показать, что Дупликатор обладает победной стратегией тогда, и только тогда, когда те же модальные высказывания, что являются истинными на s в A, истинны и на t в B.

Существует много обобщений этих результатов. Некоторые из них включают следующие понятия. Пусть Z  - это бинарное отношение, которое связывает состояние A с состояниями B. Назовем Z бисимуляцией между A и B, если Дупликатор может использовать Z в качестве недетерминированной победной стратегии в назад-вперед играх между A и B, где первая пара ходов обоих игроков является определением их начальных состояний. В компьютерной науке понятие бисимуляции является критичным для понимания A и B как систем. Это отражает тот факт, что две системы взаимодействуют со своим окружением одинаковым образом, шаг за шагом. Немного раньше компьютерных ученых, описавших эти понятия, аналогичная концепция была предложена Йоханом ван Бентемом в 1976г.

6.     Игры диалога, коммуникации и доказательства

Некоторые средневековые тексты описывают форму дебатов, называемую договором. В игре участвуют два спорщика, Оппонент и Ответчик. В начале встречи спорщики согласны на позитуме, обычно ложном утверждении. Задача Ответчика заключалась в приведении рациональных ответов на вопросы от Оппонента, в предположении, что позитум является истинным: кроме того, требовалось избегать необоснованных противоречий ему. Задача  оппонента была в попытке привести Ответчика к противоречиям. Нам хорошо известен ответ на вопрос Доукинса, но мы не знаем правил игры. Средневековые записи описывают некоторые правила игры, которых следует следовать спорщикам.

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

Не все согласны с предыдущим высказыванием. Например, Катарина Дутильх Новас в 2005г. подготовила детализированную защиту той точки зрения, что договора представляют собой выдающийся факт концептуального сходства между средневековым и современным  каркасами. Но какую бы стороны мы ни заняли в этом вопросе, эти дебаты воздействуют на одну важную линию в современных исследованиях логических игр.

Представим Е, сдающего устный экзамен по доказательству теоремы. Экзаменатор дает ей высказывание и приглашает к началу его доказательства. Если высказывание имеет форму

φ ∨ ψ

то она в праве выбрать одно из высказываний и сказать «Хорошо, я докажу это» (на самом деле экзаменатор – интуиционист, и он может настоять на выборе для доказательства одного из высказываний). С другой стороны, если высказывание выглядит

φ ∧ ψ

то экзаменатор со своей стороны может выбрать одно из них, и попросить доказать его. Если она знает, как доказать конъюнкцию, то она определенно знает, как доказать конъюнктивное выражение.

Случай  φ → ψ немного сложнее. Она, вероятно, предположит истинность φ, чтобы вывести ψ; но возможно возникновение недоразумения, если высказывания, уже записанные выше, требуется доказать и φ не доказуемо. Экзаменатор может помочь ей, сказав «я предположу истинность φ, и давайте посмотрим, вытекает ли из этого ψ». С этой точки зрения есть шанс, что она получит ψ выводом из отрицания φ; она может поменяться ролями с экзаменатором, и предложить ему показать уместность вышеописанного предположения, с целью доказательства того, что это не так. Эта симметрия не идеальна: он просил показаться истинность высказывания везде, в то время как она предлагает ему показать, что высказывание истинно хотя бы где-то. Тем не менее, здесь можно наблюдать некоторую двойственность.

Игры подобного рода оканчиваются на диалектических играх Пола Лоренца. Он показал, что с некоторым давлением можно описать правила игры, которая обладает свойством того, что Е владеет победной стратегией тогда, и только тогда, когда высказывание, которое она рассматривает в начале, является теоремой интуиционистской логики.  С уходом в сторону средневековых дебатов, он назвал Е Защитником, а других игроков – Оппонентами. Почти как в средневековых договорах, Оппонент побеждает путем подвода Защитника к моменту, когда у Защитника из возможных ходов остаются только противоречия.

Лоренцен утверждал, что правила этой игры могут быть описаны в дологическом базисе, и поэтому они формируют основы логики. К сожалению, любое обоснование должно включать в себя убедительный ответ на вопрос Доукинса, а это Лоренцен не смог предоставить. Например, он рассматривал ходы как атаки, даже в тем случаях (как, например, когда выбор экзаменатора в ситуации φ ∧ ψ), когда они больше похожи на помощь. Для закрытия этого пробела Лоренцена определенно необходимо различать позиции, когда персонаж может предоставить аргумент: утверждение, предположение, уступок, вопрос, атака или поручение чего-либо. Если действительно возможно определить все эти понятия, то в дологике есть спорный момент. Но, возможно, это и не важно. Положительная сторона заключается в том, что подобного рода детализация помогает связать диалоги с неформальной логикой, и особенно с исследованиями, целью которых является систематизация возможных структур звуковых неформальных аргументов.

В любом случае, игры Лоренцена содержат в себе важную парадигму того, что недавние теоретики доказательств назвали семантикой доказательств. Семантика доказательств придает значение не только понятию доказуемости, но и каждому отдельному шагу доказательства. Она отвечает на вопрос «Чего мы достигаем, делая этот конкретный шаг доказательства?». В 1990-ых группа работников в логической ветви компьютерных наук рассмотрела игры, которые принадлежат линейной логике и некоторым другим системам доказательств том же ключе, как и игры Лоренцена относится к интуиционистской логике. Андреас Бласс и позже Самсон Абрамский с коллегами предложили игры, которые соотносятся с частями линейной логики, но в момент написания статьи еще не было установлено точное соответствие между играми и логикой. Этот пример интересен потому, что ответ на вопрос Доукинса следовало бы дать в интуитивной интерпретации законов линейной логики, так как именно этой логике он крайне необходим. Игры Абрамского представляют ситуацию с двумя взаимодействующими системами. Он начал с игр, в которых игроки вежливо делают ходы,  поэтому в последних работах Абрамского игрокам позволяется действовать в «рассредоточенной, асинхронизированной манере», замечая друг друга только тогда, когда они хотят этого. Эти игры больше не попадают под нормальный формат логических игр, и их жизненная интерпретация ставит массу новых вопросов.

Георгий Джапаридже предложил вычислимую логику для изучения вычислений. Ее синтаксис совпадает с синтаксисом логики первого подряда с некоторыми дополнительными необычными чертами. Например, не всегда определено, какой именно игрок делает следующий ход. Понятие функции стратегий более не адекватно для описания игроков. Вместо этого Джапаридзе описывает пути «чтения» второго игрока (игрок Е в нашей интерпретации) как компьютерной машины. Более подробная информация доступна на его веб-сайте.

Другая группа игр того же семейства, что и игры Лоренцена, это игры доказательств Павела Рудлака (2000 г.). В них Оппонент (называемый Доказывающим) выступает в роли прокурора в суде, который знает, что Защитник (называемый Нарушителем) выновен в отношении некоторого вопроса. Пропонент будет настаивать на том, что тот виновен, и готов лгать для своей защиты. Цель Оппонента - атаковать Пропонента и привести его к противоречию с тем, что он сказал ранее. Но Оппонент хранит записи разговора и (как и в играх с камнями, описанными выше) вынужден иногда выбрасывать кое-что из памяти из-за недостатка места. Важным является не вопрос того, есть ли у Оппонента победная стратегия (предполагается, что есть), а то, сколько памяти ему для нее потребуется. Игры являются полезным инструментом для определения верхней и нижней границы длины доказательства в различных системах доказательств.

Другой тип логической игры, позволяющий лгать, это игры Ульма с Ложью. В них игрок загадывает число в определенном диапазоне. Целью второго игрока является найти, что это за число, задавая первому вопросы типа «да/нет». Но первому игроку разрешается несколько раз сказать ложь в своих ответах. Как и в играх Пудлака, в них точно есть победная стратегия для второго игрока, но вопрос в том, насколько тяжело будет ему выиграть. В этой игре измеряется не память, а время: как много вопросов ему нужно будет задать?

7.     Другие модельно-теоретические игры

Логические игры в этом параграфе являются инструментами математиков, но они обладают некоторыми интересными концептуальными особенностями.

Силовые игры

Силовые игры также известны как описанные теоретиками множеств как игры Банаха-Мазура (смотри ссылки на Кечриса и Окстоби ниже для получения детальной информации). Теоретики, разрабатывающие модели, используют их как способ построения бесконечный структур с контролируемыми свойствами. Для лучшего понимания представьте, что бесконечная счетная команда строителей возводит дом «А». У каждого строителя есть свое задание, например, установка ванной или поклейка обоев в холле. Каждый строитель может бесконечное число раз зайти на сайт, и заказать конечное кол-во материала для дома. Действия строителей идут по очереди, поэтому весь процесс образует последовательность шагов, занумерованных натуральными числами.

Для того чтобы показать, что дом может быть построен по всем правилам, необходимо показать, то каждый строитель в отдельности может выполнить поставленную задачу независимо от того, что делают другие рабочие. Поэтому, представим каждого строителя как игрока Е, который обладает победной стратегией в этой игре. Когда мы докажем это для каждого строителя в отдельности, то можем представить, что каждый из них выполнит свою работу в соответствии со своей победной стратегией. Они все выиграют свои игры и, в результате, построят красивый дом.

Если говорить строго, то элементы структуры А заранее фиксированы, скажем, как a₀, a₁, a₂ и т.л., но свойства элементов должны быть установлены игрой. Каждый игрок делает ход путем броска во множество атомарных или отрицаний атомарных утверждений об элементах, только с одним ограничением: множество всех выброшенных таким образом утверждений должно соответствовать фиксированному множеству аксиом, описанных перед игрой (Например, выбрасывание утверждения ¬φ подразумевает запрет всеми на использование элемента φ на последующих шагах.) В конце построенной таким образом игры множество выброшенных атомарных утверждений обладает канонической моделью, и это – структура А. Существуют способы, позволяющие гарантировать то, что эта модель обладает конечным множеством аксиом. Возможное свойство Р из А считается осуществимым, если строителю, которому дано задание сделать Р истинным в А, обладает победной стратегией. Ключевым моментом является то, что конъюнкция счетного бесконечного множества осуществимых событий тоже осуществима.

Название «силовые» пришло из приложения схожих идей Полом Коэном к конструкция моделей в теории множеств в ранних 1960-ых. Абраам Робинсон использовал их для создания основного метода построения счетных структур, а Мартин Циглер рассмотрел свойства игр. Позже Робин Хирш и Ян Ходкинсон использовали похожие игры для решения некоторых старых вопросов об относительных алгебрах.

Силовые игры являются живым примером того, что не следует забывать при размышлениях о вопросе Доукинса. Они напоминают нам о том, что в логических играх не всегда полезно рассматривать игроков как противников.

Вырезание и выбор игры

В традиционных играх выбора берется кусок пирога, и ты режешь его на две меньшие части. Затем Я выбираю один из кусочков и съедаю его, оставляя другой для тебя. Эта процедура подразумевает оказание на тебя давления для того, чтобы ты аккуратнее резал пирог. Математики, не до конца понимающие  цель упражнения, настаивают на его повторении. Поэтому, Я прошу тебя разрезать кусок, который я выбрал, на две части. Потому я выбираю одну из них; затем ты разрезаешь кусок опять, и так до бесконечности. А некоторые наиболее молчаливые математики попросят тебя разрезать торт на счетное число кусков вместо двух.

Эти игры важны в теории определений. Предположим, что у нас есть совокупность А объектов и семейство свойств S. Каждое свойство делит А на множество объектов, которые обладают этих свойством и не обладают. Пусть Е делит, начиная со всего множества А, и использует свойство S в качестве ножа. Пусть А выбирает один из кусков (подмножеств А) и отдает обратно Е на деление с помощью очередного использования семейства S, и так далее. Пусть Е, если А выберет пустой кусок. Скажем, что (A, S) имеет ранг не меньше m, если у А есть стратегия, которая гарантирует, что Е проиграет быстрее, чем за m шагов. Ранг (A, S) дает ценную информацию о семействе подмножеств А, определенном семейством S.

Вариации этой игры, допускающие деление куска на бесконечное количество меньших кусочков образуют фундаментальную ветвь в теории моделей, называемой теорией стабильности. Говоря проще, теория хороша в терминах теории стабильности, если при любом выборе модели А из теории и S (множества формул первого порядка над одной свободной переменной с параметрами из А), структура (A, S) обладает маленьким рангом. В одной из вариаций требуется, чтобы на каждом шаге Е делила на две части каждый из оставшихся на предыдущем шаге кусков, и, опять же, она проигрывает тогда, когда один из фрагментов оказывается пустым. (В этой версии А оказывается лишним.) В этом варианте ранг (A,S) называется размерностью Вапника-Черновененкиса. Это понятие используется в вычислительной теории обучения.

Games on the tree of two successor functions

Игры над деревьями из двух функция непосредственного следования

Представим дерево, которое разбито на уровни. На нижнем уровне находится один корень, и из него выходят левая и правая ветви. На следующем уровне есть два узла, по каждому на ветвь, и из каждого узла вырастает по ветви.  На следующем шаге уже 4 узла, и снова ветви дерева растут из каждого из узлов. Продолженное до бесконечности дерево такого вида называется деревом с двумя функция наследования (названное в честь левого и правого наследников). Выбирая в качестве узлов элементы и вводя два функциональных символа для левого и правого наследников, мы получаем некую структуру. Сильная теорема Майлка Рабина утверждает, что существует алгоритм, который для каждого одноместного высказывания второго порядка φ на языке, подходящем для данной структуры ответит нам на вопрос, является ли φ истинным в данной структуре. (одноместность второго порядка означает, что логика является логикой первого порядка, кроме того, что мы можем ставить кванторы над множествами элементов, но не над бинарными отношениями элементов).

Теорема Рабина обладает множеством полезных следствий. Например, Дов Габбэй использовал ее для доказательства описательности некоторых модальных логик. Но доказательство Рабина, использующее автоматы, было сложно проверить. Юрий Гуревич и Лео Гаррингтон, и независимо от них Андрей Мучник нашли более простые доказательства, в которых автомат является игроком в некоторой игре.

Этот результат Рабина является одним из наиболее влиятельных результатов, который соединил игры с автоматами. Другим примером являются игры паритета, который используются для проверки свойств модальных систем. Смотри, например, Stirling (2001 г.) глава 6; Bradfield and Stirling (2006 г.) обсуждали игры равенства для модальных μ-исчислений.

 

БИБЛИОГРАФИЯ:

…