Game semantics
From Wikipedia, the free encyclopedia
Game semantics (German: dialogische Logik) is an approach to formal semantics that grounds the concepts of truth or validity on game-theoretic concepts, such as the existence of a winning strategy for a player. 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. Since then, a number of different game semantics have been studied in logic. Shahid Rahman (Lille) and collaborators developed dialogic into a general framework for the study of logical and philosophical issues related to logical pluralism. At around 1995 this triggered a kind of Renaissance with lasting consequences. Actually this new philosophical impulse experienced a parallel renewal in the fields of theoretical computer sciences, computational linguistics, artificial intelligence and the formal semantics of programming languages triggered by the work of Johan van Benthem and collaborators in Amsterdam who looked thoroughly at the interface between logic and games. New results in linear logic by J-Y. 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. Jagadessan, G. Japaridze, E. Krabbe, L. Ong, H. Prakken, G. Sandu D. Walton, and J. Woods who placed game semantics in the center of new concept of logic in which logic is understood as a dynamic instrument of inference.
Contents |
[edit] Classical logic
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 dominant connective to pick one of its branches; play will then continue in that subformula, with whichever player controls its dominant 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 dominant 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.
Actually the formulation described above is due to Jaakko Hintikka's GTS-interpretation. The original version of classical (and intuitionistic) logic of Paul Lorenzen and Kuno Lorenz were not defined in relation to models but with the help 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 transform GTS-winning strategies for classical logic into the dialogical winning strategies and vice-versa.
All of these games are of perfect information; the two players always know the truth values of each primitive, and are aware of all preceding moves in the game.
[edit] 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" Dialogische Logik) semantics for intuitionistic logic. Andreas Blass[1] 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 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.
Shahid Rahman and Helge Rückert extended the 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.[1]
[edit] 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 quantifiers. 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. Foundational considerations have motivated the works of others, such as Japaridze's computability logic.
[edit] See also
[edit] References
[edit] Articles
- S.Abramsky and R.Jagadeesan, Games and full completeness for multiplicative linear logic. Journal of Symbolic Logic 59 (1994): 543-574.
- A.Blass, A game semantics for linear logic. Annals of Pure and Applied Logic 56 (1992): 151-166.
- G.Japaridze, Introduction to computability logic. Annals of Pure and Applied Logic 123 (2003): 1-99.
- Krabbe, E. C. W., 2001. "Dialogue Foundations: Dialogue Logic Revisited," Supplement to the Proceedings of The Aristotelian Society 75: 33-49.
- 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, From Games to Dialogues and Back: Towards a General Frame for Validity. Dans Ondrej Majer, Ahti-Veikko Pietarinen and Tero Tulenheimo (ed.) , Games: Unifying logic, Language and Philosophy,. LEUS: Springer, Part III, 2008.
http://plato.stanford.edu/entries/logic-dialogical/#Bib
[edit] 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 Logic in Games. Elsevier (2006).
- J. van Benthem, G. Heinzmann, M. Rebuschi and H. Visser (eds.) The Age of Alternative Logics. Springer (2006).ISBN 1-40-20-5011-4.
- L. Keiff Le Pluralisme Dialogique. Thesis Université de Lille3(2007).
- K. Lorenz, P. Lorenzen: Dialogische Logik, Darmstadt 1978
- P. Lorenzen: Lehrbuch der konstruktiven Wissenschaftstheorie, Stuttgart 2000 ISBN 3-476-01784-2
- R. Inhetveen: Logik. Eine dialog-orientierte Einführung., Leipzig 2003 ISBN 3-937219-02-1
- 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.
