View source for Game semantics

{{Semantics}}
'''Game semantics''' ({{langx|de|dialogische Logik}}, translated as ''[[dialogical logic]]'') is an approach to [[Formal semantics (logic)|formal semantics]] that grounds the concepts of [[truth]] or [[Validity (logic)|validity]] on [[game theory|game-theoretic]] concepts, such as the existence of a [[winning strategy]] for a player, somewhat resembling [[Socratic dialogues]] or medieval [[theory of Obligationes]].

==History==
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 theory|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 ([[Charles de Gaulle University – Lille III|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 (logician)|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 [[Samson Abramsky|S. Abramsky]], J. van Benthem, [[Andreas Blass|A. Blass]], [[Dov Gabbay|D. Gabbay]], [[Martin Hyland|M. Hyland]], [[Wilfred Hodges|W. Hodges]], R. Jagadeesan, [[Giorgi Japaridze|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 ({{harvtxt|de Queiroz|1988}}, {{harvtxt|de Queiroz|1991}}, {{harvtxt|de Queiroz|1994}}, {{harvtxt|de Queiroz|2001}}, {{harvtxt|de Queiroz|2008}}, {{harvtxt|de Queiroz|2023}}).

==Classical logic==
The simplest application of game semantics is to [[propositional logic]]. Each [[formula (logic)|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 [[disjunction]]s in the formula, and the Falsifier is likewise given ownership of all the [[Logical conjunction|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 (logic)|quantifier]] to be removed by its "owner" (the Verifier for [[existential quantifier]]s and the Falsifier for [[universal quantifier]]s) 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 [[First-order logic#Semantics|model-based (Tarskian) semantics]]. For classical first-order logic the winning strategy for the Verifier essentially consists of finding adequate [[Skolem function]]s and [[Witness (mathematics)|witnesses]]. For example, if ''S'' denotes <math>\forall x \exists y\, \phi(x,y)</math> then an [[equisatisfiable]] statement for ''S'' is <math>\exists f \forall x \, \phi(x,f(x))</math>. 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.<ref>[[Jaakko Hintikka|J. Hintikka]] and G. Sandu, 2009, "Game-Theoretical Semantics" in Keith Allan (ed.) ''Concise Encyclopedia of Semantics'', Elsevier, {{ISBN|0-08095-968-7}}, pp. 341&ndash;343</ref>

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 ([[Strategic dominance#Iterated elimination of strictly dominated strategies (IESDS)|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)<ref>{{Cite journal|last1=Genot|first1=Emmanuel J.|last2=Jacot|first2=Justine|date=2017-09-01|title=Logical Dialogues with Explicit Preference Profiles and Strategy Selection|journal=[[Journal of Logic, Language and Information]]|language=en|volume=26|issue=3|pages=261–291|doi=10.1007/s10849-017-9252-4|s2cid=37033818|issn=1572-9583|doi-access=free}}</ref> 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 value]]s 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.

== Intuitionistic logic, denotational semantics, linear logic, logical pluralism ==
The primary motivation for Lorenzen and Kuno Lorenz was to find a game-theoretic (their term was [[Dialogical logic|''dialogical'']], in German {{ill|Dialogische Logik|de}}) semantics for [[intuitionistic logic]]. [[Andreas Blass]]<ref>[http://www.math.lsa.umich.edu/~ablass/ Andreas R. Blass<!-- Bot generated title -->]</ref> was the first to point out connections between game semantics and [[linear logic]]. This line was further developed by [[Samson Abramsky]], [[Radhakrishnan Jagadeesan]], [[Pasquale Malacaria]] and independently [[Martin Hyland]] and [[Luke Ong]], who placed special emphasis on compositionality, i.e. the definition of strategies inductively on the syntax. Using game semantics, the authors mentioned above have solved the long-standing problem of defining a [[fully abstract]] model for the programming language [[Programming language for Computable Functions|PCF]]. Consequently, game semantics has led to fully abstract semantic models for a variety of programming languages, and to new semantic-directed methods of [[software verification]] by software [[model checking]].

{{ill|Shahid Rahman|fr}} and Helge Rückert extended the [[Dialogical logic|dialogical]] approach to the study of several non-classical logics such as [[modal logic]], [[relevance logic]], [[free logic]] and [[connexive logic]]. Recently, Rahman and collaborators developed the dialogical approach into a general framework aimed at the discussion of logical pluralism.

== Quantifiers ==
Foundational considerations of game semantics have been more emphasised by [[Jaakko Hintikka]] and Gabriel Sandu, especially for [[independence-friendly logic]] (IF logic, more recently ''information''-friendly logic), a logic with [[branching quantifier]]s. It was thought that the [[principle of compositionality]] fails for these logics, so that a Tarskian [[truth definition]] could not provide a suitable semantics. To get around this problem, the quantifiers were given a game-theoretic meaning. Specifically, the approach is the same as in classical propositional logic, except that the players do not always have [[perfect information]] about previous moves by the other player. [[Wilfrid Hodges]] has proposed a [[compositional semantics]] and proved it equivalent to game semantics for IF-logics.

More recently {{ill|Shahid Rahman|fr}} and the team of dialogical logic in Lille implemented dependences and independences within a dialogical framework by means of a dialogical approach to [[intuitionistic type theory]] called ''immanent reasoning''.<ref> S. Rahman, Z. McConaughey, A. Klev, N. Clerbout: ''Immanent Reasoning or Equality in Action. A Plaidoyer for the Play level''. Springer (2018). https://www.springer.com/gp/book/9783319911489.<br>
For an application of the dialogical approach to intuitionistic type theory to the ''[[axiom of choice]]'' see S. Rahman and N. Clerbout: ''Linking Games and Constructive Type Theory: Dialogical Strategies, CTT-Demonstrations and the Axiom of Choice''. Springer-Briefs (2015). https://www.springer.com/gp/book/9783319190624.</ref>

== Computability logic == 
[[Giorgi Japaridze|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 [[Paul Lorenzen|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”.<ref>[[Giorgi Japaridze|G. Japaridze]], “[https://link.springer.com/chapter/10.1007%2F978-1-4020-9374-6_11 In the beginning was game semantics]”. In: [https://www.springer.com/book/9781402093739 Games: Unifying Logic, Language and Philosophy]. O. Majer, A.-V. Pietarinen and T. Tulenheimo, eds. Springer  2009, pp.249-350.  [https://arxiv.org/abs/cs/0507045|Preprint]</ref> 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 logic|linear]] and [[Intuitionistic logic|intuitionistic]] logics turn out to be special fragments of computability logic, obtained merely by disallowing certain groups of operators or atoms.

== See also ==
* [[Computability logic]]
* [[Dependence logic]]
* [[Ehrenfeucht–Fraïssé game]]
* [[Independence-friendly logic]]
* [[Interactive computation]]
* [[Intuitionistic logic]]
* [[Ludics]]

== References ==
{{More footnotes|date=May 2010}}
{{Reflist}}

== Bibliography ==

=== Books ===
* T. Aho and A-V. Pietarinen (eds.) ''Truth and Games. Essays in honour of Gabriel Sandu''. Societas Philosophica Fennica (2006).{{ISBN|951-9264-57-4}}.
* J. van Benthem, G. Heinzmann, M. Rebuschi and H. Visser (eds.) ''The Age of Alternative Logics''. Springer (2006).{{ISBN|978-1-4020-5011-4}}.
* R. Inhetveen: ''Logik. Eine dialog-orientierte Einführung.'', Leipzig 2003 {{ISBN|3-937219-02-1}}
* L. Keiff ''Le Pluralisme Dialogique''. Thesis Université de Lille 3 (2007).
* K. Lorenz, P. Lorenzen: ''Dialogische Logik'', Darmstadt 1978
* P. Lorenzen: ''Lehrbuch der konstruktiven Wissenschaftstheorie'', Stuttgart 2000 {{ISBN|3-476-01784-2}}
* O. Majer, A.-V. Pietarinen and T. Tulenheimo  (editors). ''[https://www.springer.com/philosophy/logic/book/978-1-4020-9373-9 Games: Unifying Logic, Language and Philosophy]''. Springer (2009).
* S. Rahman, ''Über Dialogue protologische Kategorien und andere Seltenheiten''. Frankfurt 1993 {{ISBN|3-631-46583-1}}
* S. Rahman and H. Rückert (editors), ''New Perspectives in Dialogical Logic''. Synthese 127 (2001) {{issn|0039-7857}}.
*S. Rahman and N. Clerbout: ''Linking Games and Constructive Type Theory: Dialogical Strategies, CTT-Demonstrations and the Axiom of Choice''. Springer-Briefs (2015). https://www.springer.com/gp/book/9783319190624.
*S. Rahman, Z. McConaughey, A. Klev, N. Clerbout: ''Immanent Reasoning or Equality in Action. A Plaidoyer for the Play level''. Springer (2018). https://www.springer.com/gp/book/9783319911489.
* J. Redmond & M. Fontaine, How to play dialogues. An introduction to Dialogical Logic. London, College Publications (Col. Dialogues and the Games of Logic. A Philosophical Perspective N° 1). ({{ISBN|978-1-84890-046-2}})

=== Articles ===
* S. Abramsky and R. Jagadeesan, ''[https://ora.ox.ac.uk/objects/uuid:416fe169-a1bc-4afb-a768-59a47f3ae46d/download_file?file_format=pdf&safe_filename=gfc.pdf&type_of_work=Conference+item Games and full completeness for multiplicative linear logic]''. [[Journal of Symbolic Logic]] 59 (1994): 543-574.
* A. Blass, ''[https://www.sciencedirect.com/science/article/pii/0168007292900739/pdf?md5=cdfdfcea34460028a0622a0501ba5fe3&isDTMRedir=Y&pid=1-s2.0-0168007292900739-main.pdf A game semantics for linear logic]''. Annals of Pure and Applied Logic 56 (1992): 151-166.
* J.M.E.Hyland and H.L.Ong ''[https://www.sciencedirect.com/science/article/pii/S0890540100929171 On Full Abstraction for PCF: I, II, and III]''. Information and computation, 163(2), 285-408.
*E.J. Genot and J. Jacot, ''[https://link.springer.com/article/10.1007/s10849-017-9252-4 Logical Dialogues with Explicit Preference Profiles and Strategy Selection]'', ''Journal of Logic, Language and Information'' '''26''', 261–291 (2017). [[doi:10.1007/s10849-017-9252-4|doi.org/10.1007/s10849-017-9252-4]]
* D.R. Ghica, ''[http://doi.ieeecomputersociety.org/10.1109/LICS.2009.26 Applications of Game Semantics: From Program Analysis to Hardware Synthesis]''. 2009 24th Annual IEEE Symposium on Logic In Computer Science: 17-26. {{ISBN|978-0-7695-3746-7}}.
* G. Japaridze, ''[https://www.sciencedirect.com/science/article/pii/S016800720300023X/pdf?md5=17a6ad155f7b48e1a9f8185b2852a372&isDTMRedir=Y&pid=1-s2.0-S016800720300023X-main.pdf&_valck=1 Introduction to computability logic]''. Annals of Pure and Applied Logic 123 (2003): 1-99.
* G. Japaridze, ''[https://arxiv.org/abs/cs.LO/0507045 In the beginning was game semantics]''. In   Ondrej Majer, Ahti-Veikko Pietarinen and Tero Tulenheimo (editors), ''Games: Unifying logic, Language and Philosophy''. Springer (2009).
* Krabbe, E. C. W., 2001. "[https://onlinelibrary.wiley.com/doi/abs/10.1111/1467-8349.00077 Dialogue Foundations: Dialogue Logic Restituted] [title has been misprinted as "...Revisited"]," ''Supplement to the Proceedings of the Aristotelian Society 75'': 33-49.
* {{cite conference|author=H. Nickau|title=Hereditarily Sequential Functionals|book-title=Proc. Symp. Logical Foundations of Computer Science: Logic at St. Petersburg|volume=813|editor1=A. Nerode|editor2=Yu.V. Matiyasevich|series=Lecture Notes in Computer Science|publisher=[[Springer-Verlag]]|year=1994|pages=253–264|doi=10.1007/3-540-58140-5_25}} 
* {{cite journal |last=de Queiroz |first=R. |title=A Proof-Theoretic Account of Programming and the Role of Reduction Rules |date=1988 |journal=[[Dialectica]] |volume=42 |issue=4 |pages=265–282 |doi=10.1111/j.1746-8361.1988.tb00919.x |url=https://onlinelibrary.wiley.com/doi/abs/10.1111/j.1746-8361.1988.tb00919.x }}
* {{cite journal |last=de Queiroz |first=R. |title=Meaning as Grammar plus Consequences |date=1991 |journal=Dialectica |volume=45 |issue=1 |pages=83–86 |doi=10.1111/j.1746-8361.1991.tb00979.x |url=https://onlinelibrary.wiley.com/doi/abs/10.1111/j.1746-8361.1991.tb00979.x }}
* {{cite journal |last=de Queiroz |first=R. |title=Normalisation and Language Games |date=1994 |journal=Dialectica |volume=48 |issue=2 |pages=83–123 |doi=10.1111/j.1746-8361.1994.tb00107.x | url=https://onlinelibrary.wiley.com/doi/abs/10.1111/j.1746-8361.1994.tb00107.x }}
* {{cite journal |last=de Queiroz |first=R. |title=Meaning, Function, Purpose, Usefulness, Consequences – Interconnected Concepts |date=2001 |journal=Logic Journal of the IGPL |volume=9 |issue=5 |pages=693–734 |doi=10.1093/jigpal/9.5.693 | url=https://academic.oup.com/jigpal/article/9/5/693/688327 }}
* {{cite journal |last=de Queiroz |first=R. |title=On Reduction Rules, Meaning-as-use, and Proof-theoretic Semantics |date=2008 |journal=[[Studia Logica]] |volume=90  |issue=2 |pages=211–247 |doi=10.1007/s11225-008-9150-5 |s2cid=11321602 | url=https://doi.org/10.1007/s11225-008-9150-5 }}
* {{cite journal |last=de Queiroz |first=R. |title=From Tractatus to Later Writings and Back – New Implications from the ''Nachlass'' |date=2023 |journal=SATS Northern European Journal of Philosophy  |doi=10.1515/sats-2022-0016 |arxiv=2304.11203 |s2cid=258439631 | url=https://doi.org/10.1515/sats-2022-0016 }}
* S. Rahman and L. Keiff, ''On how to be a dialogician''. In Daniel Vanderken (ed.), ''Logic Thought and Action'', Springer (2005), 359-408. {{ISBN|1-4020-2616-1}}.
* S. Rahman and T. Tulenheimo,  ''[https://www.researchgate.net/profile/Shahid_Rahman3/publication/226118972_From_Games_to_Dialogues_and_Back/links/0deec51fa108b7c9a0000000/From-Games-to-Dialogues-and-Back.pdf From Games to Dialogues and Back: Towards a General Frame for Validity]''.  In Ondrej Majer, Ahti-Veikko Pietarinen and Tero Tulenheimo (editors), ''Games: Unifying logic, Language and Philosophy''. Springer (2009).
* {{cite book|editor=G. E. Mints|editor2=Reinhard Muskens|title=Games, logic, and constructive sets|year=2003|publisher=CSLI Publications|isbn=978-1-57586-449-5|author=Johan van Benthem|chapter=Logic and Game Theory: Close Encounters of the Third Kind }}

== External links ==
* [https://web.archive.org/web/20110411024825/http://www.cis.upenn.edu/~giorgi/cl.html Computability Logic Homepage]
* [http://www.gamesemantics.org/ GALOP: Workshop on Games for Logic and Programming Languages]
* [https://web.archive.org/web/20160303174250/http://www.csc.villanova.edu/~japaridz/CL/gsoll.html Game Semantics or Linear Logic?]
* {{IEP|dial-log|Dialogical Logic|Thomas Piecha}}
* {{SEP|logic-games|Logic and Games|Wilfrid Hodges}}
* {{SEP|logic-dialogical|Dialogical Logic|Laurent Keiff}}

[[Category:Logic in computer science]]
[[Category:Mathematical logic]]
[[Category:Philosophical logic]]
[[Category:Quantifier (logic)]]
[[Category:Game theory]]
[[Category:Semantics]]