Игровая семантика: от диалогической логики к динамической инференции.

Введение

Семантика игр (dialogische Logik, переведенная как диалогическая логика) — это подход к формальной семантике, который основывает понятия истины или валидности на игровых теоретических концепциях, таких как существование выигрышной стратегии для игрока, в некоторой степени напоминающих сократовские диалоги или средневековую теорию обязательств.

История

В конце 1950-х годов Пол Лоренцен первым ввёл игровую семантику для логики, и она была далее развита Куно Лоренцем. Практически одновременно с Лоренценом Яакко Хинтикка разработал модельно-теоретический подход, известный в литературе как GTS (игровая теоретическая семантика). С тех пор в логике изучается ряд различных игровых семантик. Шахид Рахман (Лилль III) и его коллеги развили диалогическую логику в общую структуру для изучения логических и философских проблем, связанных с логическим плюрализмом. Начиная с 1994 года это вызвало своего рода ренессанс с долгосрочными последствиями. Этот новый философский импульс получил параллельное развитие в области теоретической информатики, вычислительной лингвистики, искусственного интеллекта и формальной семантики языков программирования, например, в работах Йохана ван Бентема и его коллег в Амстердаме, которые тщательно исследовали интерфейс между логикой и играми, а также Ханно Никкау, который решил проблему полной абстракции в языках программирования с помощью игр. Новые результаты в линейной логике, полученные Жан-Ивом Жираром на стыке математической теории игр и логики, с одной стороны, и теории аргументации и логики, с другой, привели к работам многих других исследователей, включая С. Абрамского, Дж. ван Бентема, А. Бласса, Д. Габбая, М. Хайланда, У. Ходжеса, Р. Джагадесана, Г. Джапаридзе, Э. Краббе, Л. Онга, Х. Праккена, Г. Санду, Д. Уолтона и Дж. Вудса, которые поместили игровую семантику в центр новой концепции логики, в которой логика понимается как динамический инструмент вывода. Существует также альтернативный взгляд на теорию доказательств и теорию значения, отстаивающий парадигму Витгенштейна «значение как употребление», понимаемую в контексте теории доказательств, где так называемые правила редукции (показывающие влияние правил устранения на результат правил введения) следует рассматривать как подходящие для формализации объяснения (непосредственных) следствий, которые можно вывести из предложения, тем самым демонстрируя функцию/цель/полезность его главного связующего элемента в исчислении языка (, , , , , ,).

In the late 1950s Paul Lorenzen was the first to introduce a game semantics for logic, and it was further developed by Kuno Lorenz. At almost the same time as Lorenzen, Jaakko Hintikka developed a model theoretical approach known in the literature as GTS (game theoretical semantics). Since then, a number of different game semantics have been studied in logic. Shahid Rahman (Lille III) and collaborators developed dialogical logic into a general framework for the study of logical and philosophical issues related to logical pluralism. Beginning 1994 this triggered a kind of renaissance with lasting consequences. This new philosophical impulse experienced a parallel renewal in the fields of theoretical computer science, computational linguistics, artificial intelligence, and the formal semantics of programming languages, for instance the work of Johan van Benthem and collaborators in Amsterdam who looked thoroughly at the interface between logic and games, and Hanno Nickau who addressed the full abstraction problem in programming languages by means of games. New results in linear logic by Jean Yves Girard in the interfaces between mathematical game theory and logic on one hand and argumentation theory and logic on the other hand resulted in the work of many others, including S. Abramsky, J. van Benthem, A. Blass, D. Gabbay, M. Hyland, W. Hodges, R. Jagadeesan, G. Japaridze, E. Krabbe, L. Ong, H. Prakken, G. Sandu, D. Walton, and J. Woods, who placed game semantics at the center of a new concept in logic in which logic is understood as a dynamic instrument of inference. There has also been an alternative perspective on proof theory and meaning theory, advocating that Wittgenstein's "meaning as use" paradigm as understood in the context of proof theory, where the so called reduction rules (showing the effect of elimination rules on the result of introduction rules) should be seen as appropriate to formalise the explanation of the (immediate) consequences one can draw from a proposition, thus showing the function/purpose/usefulness of its main connective in the calculus of language (, , , , , ).

Классическая логика

Простейшее применение семантики игр – это логика высказываний. Каждая формула этого языка интерпретируется как игра между двумя игроками, известными как «Проверяющий» и «Опровергающий». Проверяющему предоставляется «владение» всеми дизъюнкциями в формуле, а Опровергающему – всеми конъюнкциями. Каждый ход игры состоит в том, чтобы позволить владельцу главного связующего выбрать одну из его ветвей; игра затем продолжается в этой подформуле, при этом игрок, контролирующий её главный связующий, делает следующий ход. Игра заканчивается, когда примитивное высказывание выбрано двумя игроками; в этот момент Проверяющий считается победителем, если полученное высказывание истинно, а Опровергающий – победителем, если оно ложно. Исходная формула считается истинной, если у Проверяющего есть выигрышная стратегия, и ложной, если у Опровергающего есть выигрышная стратегия. Если формула содержит отрицания или импликации, могут использоваться другие, более сложные методы. Например, отрицание должно быть истинным, если отрицаемое ложно, поэтому оно должно приводить к обмену ролями двух игроков. В более общем случае, семантика игр может быть применена к логике предикатов; новые правила позволяют «владельцу» главного квантора удалить его (Проверяющему для кванторов существования и Опровергающему для кванторов всеобщности) и заменить его связанную переменную во всех случаях на объект по выбору владельца, взятый из области квантификации. Следует отметить, что один контрпример опровергает универсально квантифицированное утверждение, а одного примера достаточно для подтверждения экзистенциально квантифицированного. При условии аксиомы выбора, игровая семантика для классической логики первого порядка согласуется с обычной, основанной на моделях (тарскианской) семантикой. Для классической логики первого порядка выигрышная стратегия для Проверяющего по сути заключается в нахождении адекватных функций Сколема и свидетелей. Например, если S обозначает, то эквиудовлетворимым утверждением для S является. Функция Сколема f (если она существует) фактически кодирует выигрышную стратегию для Проверяющего в отношении S, возвращая свидетеля для экзистенциальной подформулы для каждого выбора x, который может сделать Опровергающий. Вышеуказанное определение было впервые сформулировано Яакко Хинтиккой в рамках его интерпретации GTS. Оригинальная версия семантики игр для классической (и интуиционистской) логики, разработанная Полом Лоренценом и Куно Лоренцем, не была определена в терминах моделей, а в терминах выигрышных стратегий в формальных диалогах (P. Lorenzen, K. Lorenz 1978, S. Rahman and L. Keiff 2005). Шахид Рахман и Теро Туленхеймо разработали алгоритм для преобразования выигрышных стратегий GTS для классической логики в диалоговые выигрышные стратегии и наоборот. Формальные диалоги и игры GTS могут быть бесконечными и использовать правила окончания игры, а не позволять игрокам решать, когда прекратить игру. Достижение этого решения стандартными средствами стратегических выводов (итеративное исключение доминируемых стратегий или IEDS) в GTS и формальных диалогах было бы эквивалентно решению проблемы останова и превышает возможности рассуждения человеческих агентов. GTS избегает этого с помощью правила проверки формул на основе базовой модели; логические диалоги с правилом неповторения (подобным тройному повторению в шахматах). Genot и Jacot (2017) доказали, что игроки с сильно ограниченной рациональностью могут обоснованно прекратить игру без использования IEDS. Для большинства распространенных логик, включая вышеперечисленные, игры, возникающие из них, обладают полной информацией – то есть, оба игрока всегда знают истинностные значения каждого примитива и осведомлены обо всех предыдущих ходах в игре. Однако с появлением семантики игр были предложены логики, такие как логика независимости Хинтики и Санду, с естественной семантикой в терминах игр с неполной информацией.

The simplest application of game semantics is to propositional logic. Each formula of this language is interpreted as a game between two players, known as the "Verifier" and the "Falsifier". The Verifier is given "ownership" of all the disjunctions in the formula, and the Falsifier is likewise given ownership of all the conjunctions. Each move of the game consists of allowing the owner of the principal connective to pick one of its branches; play will then continue in that subformula, with whichever player controls its principal connective making the next move. Play ends when a primitive proposition has been so chosen by the two players; at this point the Verifier is deemed the winner if the resulting proposition is true, and the Falsifier is deemed the winner if it is false. The original formula will be considered true precisely when the Verifier has a winning strategy, while it will be false whenever the Falsifier has the winning strategy. If the formula contains negations or implications, other, more complicated, techniques may be used. For example, a negation should be true if the thing negated is false, so it must have the effect of interchanging the roles of the two players. More generally, game semantics may be applied to predicate logic; the new rules allow a principal quantifier to be removed by its "owner" (the Verifier for existential quantifiers and the Falsifier for universal quantifiers) and its bound variable replaced at all occurrences by an object of the owner's choosing, drawn from the domain of quantification. Note that a single counterexample falsifies a universally quantified statement, and a single example suffices to verify an existentially quantified one. Assuming the axiom of choice, the game theoretical semantics for classical first order logic agree with the usual model based (Tarskian) semantics. For classical first order logic the winning strategy for the Verifier essentially consists of finding adequate Skolem functions and witnesses. For example, if S denotes then an equisatisfiable statement for S is The Skolem function f (if it exists) actually codifies a winning strategy for the Verifier of S by returning a witness for the existential sub formula for every choice of x the Falsifier might make. The above definition was first formulated by Jaakko Hintikka as part of his GTS interpretation. The original version of game semantics for classical (and intuitionistic) logic due to Paul Lorenzen and Kuno Lorenz was not defined in terms of models but of winning strategies over formal dialogues (P. Lorenzen, K. Lorenz 1978, S. Rahman and L. Keiff 2005). Shahid Rahman and Tero Tulenheimo developed an algorithm to convert GTS winning strategies for classical logic into the dialogical winning strategies and vice versa. Formal dialogues and GTS games may be infinite and use end of play rules rather than letting players decide when to stop playing. Reaching this decision by standard means for strategic inferences (iterated elimination of dominated strategies or IEDS) would, in GTS and formal dialogues, be equivalent to solving the halting problem and exceeds the reasoning abilities of human agents. GTS avoids this with a rule to test formulas against an underlying model; logical dialogues, with a non repetition rule (similar to threefold repetition in Chess). Genot and Jacot (2017) proved that players with severely bounded rationality can reason to terminate a play without IEDS. For most common logics, including the ones above, the games that arise from them have perfect information—that is, the two players always know the truth values of each primitive, and are aware of all preceding moves in the game. However, with the advent of game semantics, logics, such as the independence friendly logic of Hintikka and Sandu, with a natural semantics in terms of games of imperfect information have been proposed.

Интуиционистская логика, денотационная семантика, линейная логика, логический плюрализм

Основной мотивацией для Лоренцена и Куно Лоренца было найти игросемантическую (их термин был «диалогической», на немецком языке – «de») семантику для интуиционистской логики. Андреас Бласс первым указал на связь между игросемантикой и линейной логикой. Это направление было далее развито Самсоном Абрамским, Радхакришнаном Джагадеесаном, Паскуалем Малакариа и независимо Мартином Хайландом и Люком Онгом, которые придавали особое значение композиционности, то есть определению стратегий индуктивно на синтаксисе. Используя игросемантику, вышеупомянутые авторы решили давнюю проблему определения полностью абстрактной модели для языка программирования PCF. Как следствие, игросемантика привела к созданию полностью абстрактных семантических моделей для различных языков программирования, а также к новым семантически ориентированным методам верификации программного обеспечения посредством проверки моделей. Фр и Хельге Рюккерт расширили диалогический подход для изучения ряда неклассических логик, таких как модальная логика, релевантная логика, свободная логика и коннексивная логика. В последнее время Рахман и его коллеги развили диалогический подход в общую структуру, направленную на обсуждение логического плюрализма.

Количественные показатели

Основополагающие соображения семантики игр получили большее развитие в работах Яакко Хинтикки и Габриэля Санду, особенно в отношении логики, дружественной независимости (логика IF, в последнее время – информационная логика), логики с разветвляющимися кванторами. Считалось, что принцип композиционности нарушается для этих логик, и поэтому тарскианское определение истины не может обеспечить адекватную семантику. Чтобы обойти эту проблему, кванторам было приписано игровое теоретическое значение. В частности, подход аналогичен классической пропозициональной логике, за исключением того, что игроки не всегда обладают полной информацией о предыдущих ходах соперника. Уилфрид Ходжес предложил композиционную семантику и доказал её эквивалентность семантике игр для логик IF. В последнее время fr и команда исследователей диалогической логики из Лилля реализовали зависимости и независимости в рамках диалогического подхода, используя диалогическую интерпретацию интуиционистской теории типов, известную как имманентное рассуждение.

Логика вычислимости

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

Japaridze’s computability logic is a game semantical approach to logic in an extreme sense, treating games as targets to be serviced by logic rather than as technical or foundational means for studying or justifying logic. Its starting philosophical point is that logic is meant to be a universal, general utility intellectual tool for ‘navigating the real world’ and, as such, it should be construed semantically rather than syntactically, because it is semantics that serves as a bridge between real world and otherwise meaningless formal systems (syntax). Syntax is thus secondary, interesting only as much as it services the underlying semantics. From this standpoint, Japaridze has repeatedly criticized the often followed practice of adjusting semantics to some already existing target syntactic constructions, with Lorenzen’s approach to intuitionistic logic being an example. This line of thought then proceeds to argue that the semantics, in turn, should be a game semantics, because games “offer the most comprehensive, coherent, natural, adequate and convenient mathematical models for the very essence of all ‘navigational’ activities of agents: their interactions with the surrounding world”. Accordingly, the logic building paradigm adopted by computability logic is to identify the most natural and basic operations on games, treat those operators as logical operations, and then look for sound and complete axiomatizations of the sets of game semantically valid formulas. On this path a host of familiar or unfamiliar logical operators have emerged in the open ended language of computability logic, with several sorts of negations, conjunctions, disjunctions, implications, quantifiers and modalities. Games are played between two agents: a machine and its environment, where the machine is required to follow only computable strategies. This way, games are seen as interactive computational problems, and the machine's winning strategies for them as solutions to those problems. It has been established that computability logic is robust with respect to reasonable variations in the complexity of allowed strategies, which can be brought down as low as logarithmic space and polynomial time (one does not imply the other in interactive computations) without affecting the logic. All this explains the name “computability logic” and determines applicability in various areas of computer science. Classical logic, independence friendly logic and certain extensions of linear and intuitionistic logics turn out to be special fragments of computability logic, obtained merely by disallowing certain groups of operators or atoms.

Статьи

С. Абрамский и Р. Джагадесан, Игры и полная полнота для мультипликативной линейной логики. Журнал символической логики 59 (1994): 543–574. А. Бласс, Семантика игры для линейной логики. Анналы чистой и прикладной логики 56 (1992): 151–166. J. M. E. Hyland и H. L. Ong, О полной абстракции для PCF: I, II и III. Information and computation, 163(2), 285–408. Э. Дж. Генот и Ж. Жако, Логические диалоги с явными профилями предпочтений и выбором стратегии. Журнал логики, языка и информации 26, 261–291 (2017). doi.org/10.1007/s10849-017-9252-4. D. R. Ghica, Приложения семантики игр: от анализа программ до синтеза аппаратного обеспечения. 24-й ежегодный симпозиум IEEE по логике в компьютерных науках, 2009: 17–26. Г. Джапаридзе, Введение в логику вычислимости. Анналы чистой и прикладной логики 123 (2003): 1–99. Г. Джапаридзе, В начале была семантика игр. В: Ондрей Маджер, Ахти Вейкко Пиетаринен и Теро Туленхеймо (ред.), Игры: объединяющие логику, язык и философию. Springer, 2009. Краббе, Э. К. В., 2001. "Основы диалога: восстановленная диалоговая логика [название ошибочно напечатано как "Пересмотренная"]," Дополнение к трудам Аристотелевского общества 75: 33–49. С. Рахман и Л. Кейфф, О том, как быть диалогом. В: Дэниел Вандеркен (ред.), Логика, мысль и действие. Springer, 2005, 359–408. С. Рахман и Т. Туленхеймо, От игр к диалогам и обратно: к общей структуре обоснования. В: Ондрей Маджер, Ахти Вейкко Пиетаринен и Теро Туленхеймо (ред.), Игры: объединяющие логику, язык и философию. Springer, 2009.