Игровая семантика ( нем . dialogische Logik , переводится как диалоговая логика ) — подход к формальной семантике , который основывает концепции истины или действительности на концепциях теории игр , таких как существование выигрышной стратегии для игрока, что несколько напоминает диалоги Сократа или средневековую теорию Obligationes .
В конце 1950-х годов Пол Лоренцен первым ввел игровую семантику для логики , и ее дальнейшее развитие провел Куно Лоренц . Почти в то же время, что и Лоренцен, Яакко Хинтикка разработал модельно-теоретический подход, известный в литературе как GTS (игровая теоретико-семантика). С тех пор в логике изучалось множество различных игровых семантик.
Шахид Рахман ( Лилль III ) и его коллеги развили диалогическую логику в общую структуру для изучения логических и философских вопросов, связанных с логическим плюрализмом . Начиная с 1994 года это вызвало своего рода ренессанс с долгосрочными последствиями. Этот новый философский импульс испытал параллельное обновление в областях теоретической информатики , вычислительной лингвистики , искусственного интеллекта и формальной семантики языков программирования , например, работа Йохана ван Бентема и его коллег в Амстердаме, которые тщательно рассмотрели интерфейс между логикой и играми, и Ханно Никау, который обратился к проблеме полной абстракции в языках программирования с помощью игр. Новые результаты в линейной логике Жана -Ива Жирара в интерфейсах между математической теорией игр и логикой, с одной стороны, и теорией аргументации и логикой, с другой стороны, привели к работам многих других, включая С. Абрамски , Дж. ван Бентема, А. Бласса , Д. Габбея , М. Хайленда , У. Ходжеса , Р. Джагадисана, Г. Джапаридзе , Э. Краббе, Л. Онга, Х. Праккена, Г. Санду, Д. Уолтона и Дж. Вудса, которые поместили игровую семантику в центр новой концепции в логике, в которой логика понимается как динамический инструмент вывода. Существует также альтернативная точка зрения на теорию доказательств и теорию значений, отстаивающая парадигму Витгенштейна «значение как использование», понимаемую в контексте теории доказательств, где так называемые правила редукции (показывающие влияние правил исключения на результат правил введения) следует рассматривать как подходящие для формализации объяснения (непосредственных) следствий, которые можно извлечь из предложения, тем самым показывая функцию/цель/полезность его основной связки в исчислении языка (de Queiroz (1988), de Queiroz (1991), de Queiroz (1994), de Queiroz (2001), de Queiroz (2008), de Queiroz (2023)).
Простейшим применением игровой семантики является пропозициональная логика . Каждая формула этого языка интерпретируется как игра между двумя игроками, известными как «Проверяющий» и «Фальсификатор». Проверяющему дается «право собственности» на все дизъюнкции в формуле, а Фальсификатору аналогично дается право собственности на все конъюнкции . Каждый ход игры состоит в том, чтобы позволить владельцу главной связки выбрать одну из ее ветвей; затем игра будет продолжена в этой подформуле, и любой игрок, контролирующий ее главную связку, сделает следующий ход. Игра заканчивается, когда примитивное предложение было выбрано двумя игроками таким образом; в этот момент Проверяющий считается победителем, если полученное предложение истинно, и Фальсификатор считается победителем, если оно ложно. Исходная формула будет считаться истинной именно тогда, когда у Проверяющего есть выигрышная стратегия , в то время как она будет ложной, когда у Фальсификатора есть выигрышная стратегия.
Если формула содержит отрицания или импликации, могут быть использованы другие, более сложные методы. Например, отрицание должно быть истинным, если отрицаемая вещь ложна, поэтому оно должно иметь эффект обмена ролями двух игроков.
В более общем смысле игровая семантика может применяться к логике предикатов ; новые правила позволяют удалять главный квантификатор его «владельцу» (Верификатору для квантификаторов существования и Фальсификатору для квантификаторов всеобщности ) и заменять его связанную переменную во всех случаях объектом по выбору владельца, взятым из области квантификации. Обратите внимание, что один контрпример фальсифицирует универсально квантифицированное утверждение, а одного примера достаточно для верификации экзистенциально квантифицированного утверждения. Предполагая аксиому выбора , теоретико-игровая семантика для классической логики первого порядка согласуется с обычной семантикой, основанной на моделях (Тарского) . Для классической логики первого порядка выигрышная стратегия для Верификатора по сути состоит в поиске адекватных функций Скулема и свидетелей . Например, если S обозначает, то равновыполнимое утверждение для S равно . Функция Скулема f (если она существует) фактически кодирует выигрышную стратегию для Проверяющего S , возвращая свидетельство для экзистенциальной подформулы для каждого выбора x, который может сделать Фальсификатор. [1]
Вышеуказанное определение было впервые сформулировано Яакко Хинтиккой как часть его интерпретации GTS. Первоначальная версия игровой семантики для классической (и интуиционистской) логики, предложенная Полом Лоренценом и Куно Лоренцом, была определена не в терминах моделей, а в терминах выигрышных стратегий по сравнению с формальными диалогами (P. Lorenzen, K. Lorenz 1978, S. Rahman и L. Keiff 2005). Шахид Рахман и Теро Туленхеймо разработали алгоритм для преобразования выигрышных стратегий GTS для классической логики в диалогические выигрышные стратегии и наоборот.
Формальные диалоги и игры GTS могут быть бесконечными и использовать правила окончания игры вместо того, чтобы позволять игрокам решать, когда прекратить игру. Достижение этого решения стандартными средствами для стратегических выводов ( итеративное устранение доминируемых стратегий или IEDS) в GTS и формальных диалогах было бы эквивалентно решению проблемы остановки и превышает способности рассуждения человеческих агентов. GTS избегает этого с помощью правила проверки формул на основе базовой модели; логические диалоги с правилом неповторения (аналогично троекратному повторению в шахматах). Жено и Жако (2017) [2] доказали, что игроки с жестко ограниченной рациональностью могут рассуждать о прекращении игры без IEDS.
Для большинства распространенных логик, включая те, что указаны выше, игры, которые возникают из них, имеют совершенную информацию — то есть, два игрока всегда знают истинностные значения каждого примитива и осведомлены обо всех предыдущих ходах в игре. Однако с появлением игровой семантики были предложены логики, такие как дружественная к независимости логика Хинтикки и Санду, с естественной семантикой в терминах игр с несовершенной информацией.
Основной мотивацией для Лоренцена и Куно Лоренца было найти теоретико-игровую (их термин был диалогический , на немецком языке Dialogische Logik ) семантику для интуиционистской логики . Андреас Бласс [3] был первым, кто указал на связи между семантикой игр и линейной логикой . Это направление было далее развито Самсоном Абрамски , Радхакришнаном Джагадисаном, Паскуале Малакарией и независимо Мартином Хайландом и Люком Онгом, которые уделили особое внимание композиционности, т. е. определению стратегий индуктивно по синтаксису. Используя семантику игр, упомянутые выше авторы решили давнюю проблему определения полностью абстрактной модели для языка программирования PCF . Следовательно, семантика игр привела к полностью абстрактным семантическим моделям для различных языков программирования и к новым семантически-направленным методам верификации программного обеспечения путем проверки моделей программного обеспечения .
Шахид Рахман и Хельге Рюккерт расширили диалогический подход на изучение нескольких неклассических логик, таких как модальная логика , релевантная логика , свободная логика и связная логика . Недавно Рахман и его коллеги развили диалогический подход в общую структуру, направленную на обсуждение логического плюрализма.
Фундаментальные соображения об игровой семантике были больше подчеркнуты Яакко Хинтиккой и Габриэлем Санду, особенно для независимо-дружественной логики (IF-логика, в последнее время информационно -дружественная логика), логики с разветвляющимися кванторами . Считалось, что принцип композиционности не работает для этих логик, так что определение истины Тарского не может обеспечить подходящую семантику. Чтобы обойти эту проблему, кванторам было дано теоретико-игровое значение. В частности, подход такой же, как и в классической пропозициональной логике, за исключением того, что игроки не всегда имеют полную информацию о предыдущих ходах другого игрока. Уилфрид Ходжес предложил композиционную семантику и доказал ее эквивалентность игровой семантике для IF-логик.
Совсем недавно Шахид Рахман и команда диалогической логики в Лилле реализовали зависимости и независимости в диалогической структуре с помощью диалогического подхода к интуиционистской теории типов, называемой имманентным рассуждением . [4]
Логика вычислимости Джапаридзе представляет собой игрово-семантический подход к логике в крайнем смысле, рассматривая игры как цели, которые должны обслуживаться логикой, а не как технические или основополагающие средства для изучения или обоснования логики. Ее исходная философская точка заключается в том, что логика должна быть универсальным интеллектуальным инструментом общего назначения для «навигации по реальному миру» и, как таковая, ее следует толковать семантически, а не синтаксически, поскольку именно семантика служит мостом между реальным миром и в противном случае бессмысленными формальными системами (синтаксисом). Синтаксис, таким образом, вторичен, интересен лишь в той мере, в какой он обслуживает лежащую в основе семантику. С этой точки зрения Джапаридзе неоднократно критиковал часто применяемую практику подгонки семантики под некоторые уже существующие целевые синтаксические конструкции, примером чего является подход Лоренцена к интуиционистской логике. Эта линия мысли затем переходит к утверждению, что семантика, в свою очередь, должна быть игровой семантикой, потому что игры «предлагают наиболее всеобъемлющие, связные, естественные, адекватные и удобные математические модели для самой сути всех «навигационных» действий агентов: их взаимодействия с окружающим миром». [5] Соответственно, парадигма построения логики, принятая логикой вычислимости, заключается в выявлении наиболее естественных и базовых операций в играх, обработке этих операторов как логических операций, а затем поиске надежных и полных аксиоматизаций множеств игровых семантически допустимых формул. На этом пути в открытом языке логики вычислимости появилось множество знакомых или незнакомых логических операторов с несколькими видами отрицаний, конъюнкций, дизъюнкций, импликаций, квантификаторов и модальностей.
Игры ведутся между двумя агентами: машиной и ее окружением, где от машины требуется следовать только вычислимым стратегиям. Таким образом, игры рассматриваются как интерактивные вычислительные задачи, а выигрышные стратегии машины для них — как решения этих задач. Установлено, что логика вычислимости устойчива по отношению к разумным вариациям сложности разрешенных стратегий, которые могут быть снижены до логарифмического пространства и полиномиального времени (одно не подразумевает другое в интерактивных вычислениях) без ущерба для логики. Все это объясняет название «логика вычислимости» и определяет применимость в различных областях компьютерной науки. Классическая логика , логика, дружественная к независимости , и некоторые расширения линейной и интуиционистской логики оказываются особыми фрагментами логики вычислимости, полученными просто путем запрета определенных групп операторов или атомов.
