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. 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, intuitionistic logic, linear logic, and modal logic. The approach bears conceptual resemblances to ancient Socratic dialogues, medieval theory of Obligationes, and constructive mathematics. Since the 1990s, game semantics has found important applications in theoretical computer science, particularly in the semantics of programming languages, concurrency theory, and the study of computational complexity.

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 (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, computational linguistics, artificial intelligence, and the formal semantics of programming languages, for instance the work of 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 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 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 (de Queiroz (1988), de Queiroz (1991), de Queiroz (1994), de Queiroz (2001), de Queiroz (2008), de Queiroz (2023), de Queiroz (2025a), de Queiroz (2025b)).

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 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 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. Assuming the axiom of choice, the game-theoretical semantics for classical first-order logic 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. For example, if S denotes ${\displaystyle \forall x\exists y\,\phi (x,y)}$ then an equisatisfiable statement for S is ${\displaystyle \exists f\forall x\,\phi (x,f(x))}$. 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.