Game semantics
Encyclopedia
Game semantics 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, somewhat resembling Socratic dialogues or medieval theory of Obligationes
. 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 science
, 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.
. 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.
. Andreas Blass
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.
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. Foundational considerations have motivated the works of others, such as Japaridze's computability logic
.
Truth
Truth has a variety of meanings, such as the state of being in accord with fact or reality. It can also mean having fidelity to an original or to a standard or ideal. In a common usage, it also means constancy or sincerity in action or character...
or validity
Validity
In logic, argument is valid if and only if its conclusion is entailed by its premises, a formula is valid if and only if it is true under every interpretation, and an argument form is valid if and only if every argument of that logical form is valid....
on game-theoretic
Game theory
Game theory is a mathematical method for analyzing calculated circumstances, such as in games, where a person’s success is based upon the choices of others...
concepts, such as the existence of a winning strategy for a player, somewhat resembling Socratic dialogues or medieval theory of Obligationes
Theory of Obligationes
Obligationes or disputations de obligationibus were a medieval disputation format common in the XIIIth and XIVth centuries, which had nothing to do with ethics or morals but rather with logical formalisms. The name comes from the fact that the participants were "obliged" to follow the rules...
. In the late 1950s Paul Lorenzen
Paul Lorenzen
Paul Lorenzen was a philosopher andmathematician.As a founder of the Erlangen School and the inventor of game semantics he was a famous German philosopher of the 20th century.-Biography:Lorenzen studied with David Hilbert as a schoolboy and he was one of Hasse's...
was the first to introduce a game semantics for logic
Logic
In philosophy, Logic is the formal systematic study of the principles of valid inference and correct reasoning. Logic is used in most intellectual activities, but is studied primarily in the disciplines of philosophy, mathematics, semantics, and computer science...
, and it was further developed by Kuno Lorenz. At almost the same time as Lorenzen, Jaakko Hintikka
Jaakko Hintikka
Kaarlo Jaakko Juhani Hintikka is a Finnish philosopher and logician.Hintikka was born in Vantaa. After teaching for a number of years at Florida State University, Stanford, University of Helsinki, and the Academy of Finland, he is currently Professor of Philosophy at Boston University...
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 science
Theoretical computer science
Theoretical computer science is a division or subset of general computer science and mathematics which focuses on more abstract or mathematical aspects of computing....
, computational linguistics
Computational linguistics
Computational linguistics is an interdisciplinary field dealing with the statistical or rule-based modeling of natural language from a computational perspective....
, artificial intelligence
Artificial intelligence
Artificial intelligence is the intelligence of machines and the branch of computer science that aims to create it. AI textbooks define the field as "the study and design of intelligent agents" where an intelligent agent is a system that perceives its environment and takes actions that maximize its...
and the formal semantics of programming languages
Formal semantics of programming languages
In programming language theory, semantics is the field concerned with the rigorous mathematical study of the meaning of programming languages and models of computation...
triggered by the work of Johan van Benthem
Johan van Benthem (logician)
Johannes Franciscus Abraham Karel van Benthem is a University Professor of logic at the University of Amsterdam at the Institute for Logic, Language and Computation and professor of philosophy at Stanford University . He was awarded the Spinozapremie in 1996.He studied physics , philosophy...
and collaborators in Amsterdam
Amsterdam
Amsterdam is the largest city and the capital of the Netherlands. The current position of Amsterdam as capital city of the Kingdom of the Netherlands is governed by the constitution of August 24, 1815 and its successors. Amsterdam has a population of 783,364 within city limits, an urban population...
who looked thoroughly at the interface between logic and games. New results in linear logic
Linear logic
Linear logic is a substructural logic proposed by Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter...
by J-Y. Girard in the interfaces between mathematical game theory and logic
Logic
In philosophy, Logic is the formal systematic study of the principles of valid inference and correct reasoning. Logic is used in most intellectual activities, but is studied primarily in the disciplines of philosophy, mathematics, semantics, and computer science...
on one hand and argumentation theory
Argumentation theory
Argumentation theory, or argumentation, is the interdisciplinary study of how humans should, can, and do reach conclusions through logical reasoning, that is, claims based, soundly or not, on premises. It includes the arts and sciences of civil debate, dialogue, conversation, and persuasion...
and logic on the other hand resulted in the work of many others, including S. Abramsky
Samson Abramsky
Samson D. Abramsky FRS, FRSE is a computer scientist who currently holds the Christopher Strachey Professorship at Oxford University Computing Laboratory. He is well known for playing a leading role in the development of game semantics...
, J. van Benthem, A. Blass
Andreas Blass
Andreas Raphael Blass is a mathematician, currently a professor at the University of Michigan. He specializes in mathematical logic, particularly set theory, and theoretical computer science....
, D. Gabbay
Dov Gabbay
Dov M. Gabbay is Augustus De Morgan Professor of Logic at the Group of Logic, Language and Computation, Department of Computer Science, King's College London . He has authored over four hundred and fifty research papers and over thirty research monographs...
, M. Hyland
Martin Hyland
John Martin Elliott Hyland is professor of mathematics at King's College in the University of Cambridge, England where he is currently head of the Department of Pure Mathematics and Mathematical Statistics...
, W. Hodges, R. Jagadessan, G. Japaridze
Giorgi Japaridze
Giorgi Japaridze is a logician, at Villanova University in Villanova, Pennsylvania. In the past his contributions were primarily into the areas of provability logic and interpretability logic...
, 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.
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 conjunctionsLogical conjunction
In logic and mathematics, a two-place logical operator and, also known as logical conjunction, results in true if both of its operands are true, otherwise the value of false....
. 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
Negation
In logic and mathematics, negation, also called logical complement, is an operation on propositions, truth values, or semantic values more generally. Intuitively, the negation of a proposition is true when that proposition is false, and vice versa. In classical logic negation is normally identified...
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
Predicate logic
In mathematical logic, predicate logic is the generic term for symbolic formal systems like first-order logic, second-order logic, many-sorted logic or infinitary logic. This formal system is distinguished from other systems in that its formulae contain variables which can be quantified...
; 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
Perfect information
In game theory, perfect information describes the situation when a player has available the same information to determine all of the possible games as would be available at the end of the game....
; the two players always know the truth values of each primitive, and are aware of all preceding moves in the game.
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 logicIntuitionistic logic
Intuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...
. Andreas Blass
Andreas Blass
Andreas Raphael Blass is a mathematician, currently a professor at the University of Michigan. He specializes in mathematical logic, particularly set theory, and theoretical computer science....
was the first to point out connections between game semantics and linear logic
Linear logic
Linear logic is a substructural logic proposed by Jean-Yves Girard as a refinement of classical and intuitionistic logic, joining the dualities of the former with many of the constructive properties of the latter...
. This line was further developed by Samson Abramsky
Samson Abramsky
Samson D. Abramsky FRS, FRSE is a computer scientist who currently holds the Christopher Strachey Professorship at Oxford University Computing Laboratory. He is well known for playing a leading role in the development of game semantics...
, Radhakrishnan Jagadeesan, Pasquale Malacaria and independently Martin Hyland
Martin Hyland
John Martin Elliott Hyland is professor of mathematics at King's College in the University of Cambridge, England where he is currently head of the Department of Pure Mathematics and Mathematical Statistics...
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
Programming language for Computable Functions
In computer science, Programming Computable Functions,"PCF is a programming language for computable functions, based on LCF, Scott’s logic of computable functions" . Programming Computable Functions is used by . It is also referred to as Programming with Computable Functions or Programming language...
. 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
Model checking
In computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....
.
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.
Quantifiers
Foundational considerations of game semantics have been more emphasised by Jaakko HintikkaJaakko Hintikka
Kaarlo Jaakko Juhani Hintikka is a Finnish philosopher and logician.Hintikka was born in Vantaa. After teaching for a number of years at Florida State University, Stanford, University of Helsinki, and the Academy of Finland, he is currently Professor of Philosophy at Boston University...
and Gabriel Sandu, especially for Independence-friendly logic
Independence-friendly logic
Independence-friendly logic , proposed by Jaakko Hintikka and Gabriel Sandu, aims at being a more natural and intuitive alternative to classical first-order logic . IF logic is characterized by branching quantifiers...
(IF logic, more recently Information-friendly logic), a logic with branching quantifier
Branching quantifier
In logic a branching quantifier, also called a Henkin quantifier, finite partially ordered quantifier or even nonlinear quantifier, is a partial ordering\langle Qx_1\dots Qx_n\rangle...
s. It was thought that the principle of compositionality
Principle of compositionality
In mathematics, semantics, and philosophy of language, the Principle of Compositionality is the principle that the meaning of a complex expression is determined by the meanings of its constituent expressions and the rules used to combine them. This principle is also called Frege's Principle,...
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
Perfect information
In game theory, perfect information describes the situation when a player has available the same information to determine all of the possible games as would be available at the end of the game....
about previous moves by the other player. Wilfrid Hodges
Wilfrid Hodges
Wilfrid Augustine Hodges is a British mathematician, known for his work in model theory. He was Professor of Mathematics at Queen Mary, University of London from 1987 to 2006, and is the author of numerous books on logic....
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
Computability logic
Introduced by Giorgi Japaridze in 2003, computability logic is a research programme and mathematical framework for redeveloping logic as a systematic formal theory of computability, as opposed to classical logic which is a formal theory of truth...
.
See also
- Independence-friendly logicIndependence-friendly logicIndependence-friendly logic , proposed by Jaakko Hintikka and Gabriel Sandu, aims at being a more natural and intuitive alternative to classical first-order logic . IF logic is characterized by branching quantifiers...
- Dependence logic
- Intuitionistic logicIntuitionistic logicIntuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...
- Computability logicComputability logicIntroduced by Giorgi Japaridze in 2003, computability logic is a research programme and mathematical framework for redeveloping logic as a systematic formal theory of computability, as opposed to classical logic which is a formal theory of truth...
- Interactive computationInteractive computationIn computer science, interactive computation is a mathematical model for computation that involves communication with the external world during the computation...
- LudicsLudicsIn proof theory, ludics is an analysis of the principles governing inference rules of mathematical logic. Key features of ludics are its notion of compound connectives using a technique known as focusing or focalisation , and its use of locations or loci over a base instead of propositions.More...
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.
- D.R. Ghica, 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, Introduction to computability logic. Annals of Pure and Applied Logic 123 (2003): 1-99.
- G. Japaridze, 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. "Dialogue Foundations: Dialogue Logic Restituted [title has been misprinted as "...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. In Ondrej Majer, Ahti-Veikko Pietarinen and Tero Tulenheimo (editors), Games: Unifying logic, Language and Philosophy. Springer (2009).
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 1-40-20-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 Lille3(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). 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.