Game semantics is an approach to
formal semantics that grounds the concepts of
truth
Truth or verity is the Property (philosophy), property of being in accord with fact or reality.Merriam-Webster's Online Dictionarytruth, 2005 In everyday language, it is typically ascribed to things that aim to represent reality or otherwise cor ...
or
validity on
game-theoretic concepts, such as the existence of a
winning strategy for a player. In this framework, logical formulas are interpreted as defining games between two players. The term encompasses several related but distinct traditions, including
dialogical logic (developed by
Paul Lorenzen and
Kuno Lorenz in Germany starting in the 1950s) and game-theoretical semantics (developed by
Jaakko Hintikka in Finland).
Game semantics represents a significant departure from traditional
model-theoretic approaches by emphasizing the dynamic, interactive nature of logical reasoning rather than static truth assignments. It provides intuitive interpretations for various logical systems, including
classical logic
Classical logic (or standard logic) or Frege–Russell logic is the intensively studied and most widely used class of deductive logic. Classical logic has had much influence on analytic philosophy.
Characteristics
Each logical system in this c ...
,
intuitionistic logic
Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems ...
,
linear logic, and
modal logic
Modal logic is a kind of logic used to represent statements about Modality (natural language), necessity and possibility. In philosophy and related fields
it is used as a tool for understanding concepts such as knowledge, obligation, and causality ...
. The approach bears conceptual resemblances to ancient
Socratic dialogues
Socratic dialogue () is a genre of literary prose developed in Ancient Greece, Greece at the turn of the fourth century BC. The earliest ones are preserved in the works of Plato and Xenophon and all involve Socrates as the protagonist. These dial ...
, medieval
theory of Obligationes, and
constructive mathematics
In the philosophy of mathematics, constructivism asserts that it is necessary to find (or "construct") a specific example of a mathematical object in order to prove that an example exists. Contrastingly, in classical mathematics, one can prove th ...
. Since the 1990s, game semantics has found important applications in
theoretical computer science
Theoretical computer science is a subfield of computer science and mathematics that focuses on the Abstraction, abstract and mathematical foundations of computation.
It is difficult to circumscribe the theoretical areas precisely. The Associati ...
, particularly in the semantics of
programming languages
A programming language is a system of notation for writing computer programs.
Programming languages are described in terms of their syntax (form) and semantics (meaning), usually defined by a formal language. Languages usually provide features ...
,
concurrency theory, and the study of
computational complexity
In computer science, the computational complexity or simply complexity of an algorithm is the amount of resources required to run it. Particular focus is given to computation time (generally measured by the number of needed elementary operations ...
.
History
In the late 1950s
Paul Lorenzen was the first to introduce a game semantics for
logic
Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the study of deductively valid inferences or logical truths. It examines how conclusions follow from premises based on the structure o ...
, 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
Theoretical computer science is a subfield of computer science and mathematics that focuses on the Abstraction, abstract and mathematical foundations of computation.
It is difficult to circumscribe the theoretical areas precisely. The Associati ...
,
computational linguistics
Computational linguistics is an interdisciplinary field concerned with the computational modelling of natural language, as well as the study of appropriate computational approaches to linguistic questions. In general, computational linguistics ...
,
artificial intelligence
Artificial intelligence (AI) is the capability of computer, computational systems to perform tasks typically associated with human intelligence, such as learning, reasoning, problem-solving, perception, and decision-making. It is a field of re ...
, and the
formal semantics of programming languages
In programming language theory, semantics is the rigorous mathematical study of the meaning of programming languages. Semantics assigns computational meaning to valid string (computer science), strings in a programming language syntax. It is cl ...
, for instance the work of
Johan van Benthem and collaborators in
Amsterdam
Amsterdam ( , ; ; ) is the capital of the Netherlands, capital and Municipalities of the Netherlands, largest city of the Kingdom of the Netherlands. It has a population of 933,680 in June 2024 within the city proper, 1,457,018 in the City Re ...
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
Jean-Yves Girard (; born 1947) is a French logician working in proof theory. He is a research director (emeritus) at the mathematical institute of University of Aix-Marseille, at Luminy.
Biography
Jean-Yves Girard is an alumnus of the Éc ...
in the interfaces between mathematical game theory and
logic
Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the study of deductively valid inferences or logical truths. It examines how conclusions follow from premises based on the structure o ...
on one hand and
argumentation theory
Argumentation theory is the interdisciplinary study of how conclusions can be supported or undermined by premises through logical reasoning. With historical origins in logic, dialectic, and rhetoric, argumentation theory includes the arts and scie ...
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
Proof theory is a major branchAccording to , proof theory is one of four domains mathematical logic, together with model theory, axiomatic set theory, and recursion theory. consists of four corresponding parts, with part D being about "Proof The ...
and meaning theory, advocating that
Wittgenstein
Ludwig Josef Johann Wittgenstein ( ; ; 26 April 1889 – 29 April 1951) was an Austrian philosopher who worked primarily in logic, the philosophy of mathematics, the philosophy of mind, and the philosophy of language.
From 1929 to 1947, Witt ...
'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 (, , , , , ).
Classical logic
The simplest application of game semantics is to
propositional logic
The propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. Sometimes, it is called ''first-order'' propositional logic to contra ...
. Each
formula
In science, a formula is a concise way of expressing information symbolically, as in a mathematical formula or a ''chemical formula''. The informal use of the term ''formula'' in science refers to the general construct of a relationship betwe ...
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
In logic, disjunction (also known as logical disjunction, logical or, logical addition, or inclusive disjunction) is a logical connective typically notated as \lor and read aloud as "or". For instance, the English language sentence "it is ...
s 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
In logic, negation, also called the logical not or logical complement, is an operation (mathematics), operation that takes a Proposition (mathematics), proposition P to another proposition "not P", written \neg P, \mathord P, P^\prime or \over ...
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
First-order logic, also called predicate logic, predicate calculus, or quantificational logic, is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables ove ...
; the new rules allow a principal
quantifier to be removed by its "owner" (the Verifier for
existential quantifier
Existentialism is a family of philosophy, philosophical views and inquiry that explore the human individual's struggle to lead an Authenticity (philosophy), authentic life despite the apparent Absurdity#The Absurd, absurdity or incomprehensibili ...
s and the Falsifier for
universal quantifier
In mathematical logic, a universal quantification is a type of quantifier, a logical constant which is interpreted as "given any", "for all", "for every", or "given an arbitrary element". It expresses that a predicate can be satisfied by e ...
s) and its
bound variable
In mathematics, and in other disciplines involving formal languages, including mathematical logic and computer science, a variable may be said to be either free or bound. Some older books use the terms real variable and apparent variable for f ...
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
In mathematics, the axiom of choice, abbreviated AC or AoC, is an axiom of set theory. Informally put, the axiom of choice says that given any collection of non-empty sets, it is possible to construct a new set by choosing one element from e ...
, the game-theoretical semantics for classical
first-order logic
First-order logic, also called predicate logic, predicate calculus, or quantificational logic, is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over ...
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
In law, a witness is someone who, either voluntarily or under compulsion, provides testimonial evidence, either oral or written, of what they know or claim to know.
A witness might be compelled to provide testimony in court, before a grand jur ...
. 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
In computability theory (computer science), computability theory, the halting problem is the problem of determining, from a description of an arbitrary computer program and an input, whether the program will finish running, or continue to run for ...
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
Bounded rationality is the idea that rationality is limited when individuals decision-making, make decisions, and under these limitations, rational individuals will select a decision that is satisficing, satisfactory rather than optimal.
Limitat ...
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
Perfect information is a concept in game theory and economics that describes a situation where all players in a game or all participants in a market have knowledge of all relevant information in the system. This is different than complete informat ...
—that is, the two players always know the
truth value
In logic and mathematics, a truth value, sometimes called a logical value, is a value indicating the relation of a proposition to truth, which in classical logic has only two possible values ('' true'' or '' false''). Truth values are used in ...
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'', in German ) semantics for
intuitionistic logic
Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems ...
.
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
(John) Martin Elliott Hyland is professor of mathematical logic at the University of Cambridge and a fellow of King's College, Cambridge. His interests include mathematical logic, category theory, and theoretical computer science.
Education
Hy ...
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 Software verification is a discipline of software engineering, programming languages, and theory of computation whose goal is to assure that software satisfies the expected requirements.
Broad scope and classification
A broad definition of verif ...
by software
model checking.
and Helge Rückert extended the
dialogical approach to the study of several non-classical logics such as
modal logic
Modal logic is a kind of logic used to represent statements about Modality (natural language), necessity and possibility. In philosophy and related fields
it is used as a tool for understanding concepts such as knowledge, obligation, and causality ...
,
relevance logic
Relevance logic, also called relevant logic, is a kind of non-classical logic requiring the antecedent and consequent of implications to be relevantly related. They may be viewed as a family of substructural or modal logics. It is generally, b ...
,
free logic
A free logic is a logic with fewer existential presuppositions than classical logic. Free logics may allow for terms that do not denote any object. Free logics may also allow models that have an empty domain. A free logic with the latter propert ...
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 quantifiers. It was thought that the
principle of compositionality
In semantics, mathematical logic and related disciplines, 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. ...
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 is a concept in game theory and economics that describes a situation where all players in a game or all participants in a market have knowledge of all relevant information in the system. This is different than complete informat ...
about previous moves by the other player.
Wilfrid Hodges
Wilfrid Augustine Hodges, Fellow of the British Academy, FBA (born 27 May 1941) is a British mathematician and logic, logician known for his work in model theory.
Life
Hodges attended New College, Oxford (1959–65), where he received degrees i ...
has proposed a
compositional semantics and proved it equivalent to game semantics for IF-logics.
More recently 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
Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory (MLTT)) is a type theory and an alternative foundation of mathematics.
Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematicia ...
called ''immanent reasoning''.
Computability logic
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”.
[ G. Japaridze, �]
In the beginning was game semantics
��. In
Games: Unifying Logic, Language and Philosophy
O. Majer, A.-V. Pietarinen and T. Tulenheimo, eds. Springer 2009, pp.249-350.
/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
In theoretical computer science, the time complexity is the computational complexity that describes the amount of computer time it takes to run an algorithm. Time complexity is commonly estimated by counting the number of elementary operations p ...
(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
Classical logic (or standard logic) or Frege–Russell logic is the intensively studied and most widely used class of deductive logic. Classical logic has had much influence on analytic philosophy.
Characteristics
Each logical system in this c ...
, independence-friendly logic and certain extensions of linear
In mathematics, the term ''linear'' is used in two distinct senses for two different properties:
* linearity of a '' function'' (or '' mapping'');
* linearity of a '' polynomial''.
An example of a linear function is the function defined by f(x) ...
and 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
Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems ...
* Ludics
References
Bibliography
Books
* T. Aho and A-V. Pietarinen (eds.) ''Truth and Games. Essays in honour of Gabriel Sandu''. Societas Philosophica Fennica (2006)..
* J. van Benthem, G. Heinzmann, M. Rebuschi and H. Visser (eds.) ''The Age of Alternative Logics''. Springer (2006)..
* R. Inhetveen: ''Logik. Eine dialog-orientierte Einführung.'', Leipzig 2003
* 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
* 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
* S. Rahman and H. Rückert (editors), ''New Perspectives in Dialogical Logic''. Synthese 127 (2001) .
*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). ()
Articles
* S. Abramsky and R. Jagadeesan,
Games and full completeness for multiplicative linear logic
'. Journal of Symbolic Logic
The '' Journal of Symbolic Logic'' is a peer-reviewed mathematics journal published quarterly by Association for Symbolic Logic. It was established in 1936 and covers mathematical logic. The journal is indexed by '' Mathematical Reviews'', Zent ...
59 (1994): 543-574.
* A. Blass,
A game semantics for linear logic
'. Annals of Pure and Applied Logic 56 (1992): 151-166.
* J.M.E.Hyland and H.L.Ong
On Full Abstraction for PCF: I, II, and III
'. Information and computation, 163(2), 285-408.
*E.J. Genot and J. Jacot,
Logical Dialogues with Explicit Preference Profiles and Strategy Selection
', ''Journal of Logic, Language and Information'' 26, 261–291 (2017). doi.org/10.1007/s10849-017-9252-4
* 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. .
* 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
itle 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. .
* 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).
*
External links
GALOP: Workshop on Games for Logic and Programming Languages
*
*
* {{SEP, logic-dialogical, Dialogical Logic, Laurent Keiff
Logic in computer science
Mathematical logic
Philosophical logic
Quantifier (logic)
Game theory
Semantics