Game-theoretic semantics

Game-theoretic semantics is an approach to logical semantics that interprets the meaning of a formula as a game between two players: the 'verifier' (or proponent), who tries to show that the formula is true, and the 'falsifier' (or opponent), who tries to show that it is false. The approach was developed by Paul Lorenzen in the 1950s and later refined by Jaakko Hintikka, and it provides a procedural, interactive alternative to the static truth-conditional semantics of model theory.

In a game-theoretic interpretation, a disjunction is a choice for the verifier: she chooses which disjunct to defend. A conjunction is a choice for the falsifier: he chooses which conjunct to attack. An existential quantifier is a choice of a witness by the verifier; a universal quantifier is a choice of a counterexample by the falsifier. Negation swaps the roles of the players. The formula is true if the verifier has a winning strategy, false if the falsifier has one.

This framework reveals that the logical connectives are not merely compositional building blocks but moves in a rule-governed game. The logical connective is a strategic choice, and the meaning of a formula is the set of winning strategies available to the verifier. This connects logic to game theory in a deep way: the semantics of a language is a game, and the pragmatics of using the language is the play of the game.

Game-theoretic semantics has been extended to natural language (where it handles anaphora, quantifier scope, and focus), to computer science (where it underlies the game semantics of programming languages and the verification of open systems), and to philosophical logic (where it provides a foundation for dialogical logic and the study of argumentation). It is also the semantic counterpart of the Curry-Howard correspondence: just as proofs are programs, strategies are proofs, and the game is the computational process of verification itself.

The open question is whether game-theoretic semantics can be extended to handle genuinely non-deterministic or probabilistic systems, where the verifier's strategy must be not just winning but robust against randomness. This would connect the framework to the study of stochastic games, reinforcement learning, and the verification of AI systems that operate in uncertain environments.