Game semantics (German: dialogische Logik, translated as dialogical logic) 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.
At almost the same time as Lorenzen, Jaakko Hintikka developed a model-theoretical approach known in the literature as GTS (game-theoretical semantics).
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.
For classical first-order logic the winning strategy for the Verifier essentially consists of finding adequate Skolem functions and witnesses.
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.
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 and exceeds the reasoning abilities of human agents.
Genot and Jacot (2017)[2] proved that players with severely bounded rationality can reason to terminate a play without IEDS.
The primary motivation for Lorenzen and Kuno Lorenz was to find a game-theoretic (their term was dialogical, in German Dialogische Logik [de]) semantics for intuitionistic 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.
Recently, Rahman and collaborators developed the dialogical approach into a general framework aimed at the discussion of logical pluralism.
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.