Editing Game semantics (section)

==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.