Game Semantics
Origin. Lorenzen's dialogical logic (1960s). Hintikka's game-theoretic semantics (1970s). Abramsky, Jagadeesan, Malacaria: full abstraction (1990s). Games between Proponent (verifier) and Opponent (falsifier). Foundation for programming language semantics.
Models. Truth as winning strategy. Formula φ is true iff Proponent has winning strategy in game G(φ). Opponent challenges, Proponent defends. ∨: Proponent chooses disjunct. ∧: Opponent chooses conjunct. ∀: Opponent chooses witness. ∃: Proponent chooses witness.
Formalism.
Semantic games (Hintikka): G(φ, M, s): game for φ in model M, assignment s.
- G(p): Proponent wins if p true under s.
- G(φ ∨ ψ): Proponent chooses φ or ψ, plays that game.
- G(φ ∧ ψ): Opponent chooses, Proponent plays.
- G(∃x.φ): Proponent picks a, plays G(φ[a/x]).
- G(∀x.φ): Opponent picks a, plays G(φ[a/x]).
- G(¬φ): roles switch, play G(φ).
Winning: M ⊨ φ iff Proponent has winning strategy in G(φ, M).
Full abstraction (PCF): Arena: set of moves with Player/Opponent labeling. Strategy: set of plays respecting alternation. Composition: strategy composition = function composition. Achieves: two terms equal iff same strategy.
Innocent strategies: Strategy depends only on P-view (justification pointers). Models pure functional computation.
Arena structure: Moves labeled: question/answer, O/P. Bracketing: answers respond to questions. Innocence, well-bracketing, visibility constraints.
Symbols.
| Symbol | Unicode | Name | Meaning |
|---|---|---|---|
| σ | U+03C3 | Sigma / Strategy | A set of plays; the denotation of a proof or program |
| ⊛ | U+229B | Circled asterisk / Composition | Composition of strategies, matching function composition |
| ⟦ ⟧ | U+27E6, U+27E7 | Semantic brackets | ⟦M⟧ is the strategy denoting M |
| ⊨ | U+22A8 | Entailment | M ⊨ φ: Proponent has a winning strategy in G(φ, M) |
| φ, ψ | U+03C6, U+03C8 | Phi, Psi | Formulas whose games are being played |
| ¬ | U+00AC | Negation | Swaps the roles of Proponent and Opponent |
| ∨ | U+2228 | Disjunction | Proponent chooses the disjunct |
| ∧ | U+2227 | Conjunction | Opponent chooses the conjunct |
| ∃ | U+2203 | Existential quantifier | Proponent supplies the witness |
| ∀ | U+2200 | Universal quantifier | Opponent supplies the witness |
| P | — | Proponent | Verifier; Player, in the programming-language reading |
| O | — | Opponent | Falsifier; the environment |
| q, a | — | Question, Answer | Move labels constrained by well-bracketing |
Metatheory. Hintikka's semantic games recast Tarskian truth, and the payoff is that varying the players' information changes the logic: independence-friendly logic, where a quantifier may be independent of an earlier one, has exactly the expressive power of Σ¹₁ (Walkoe; Enderton), hence by Fagin's theorem captures NP on finite structures. Lorenzen's dialogical games were given a precise formulation by Felscher (1985), who proved that Proponent has a winning strategy in the intuitionistic dialogue game for φ exactly when φ is intuitionistically valid. The programming-language line runs deepest: Abramsky, Jagadeesan and Malacaria, and independently Hyland and Ong, built fully abstract models of PCF from innocent, well-bracketed strategies (both published in 2000), settling the problem Plotkin raised in 1977. Relaxing the constraints classifies effects — dropping innocence models mutable state (Abramsky, Honda and McCusker, 1998), dropping well-bracketing models control operators (Laird, 1997).
Applies to. Programming language semantics. Full abstraction proofs. Program equivalence. Concurrency models. Linear logic semantics. Verification via games. Dialogue systems.
Limitations. Full abstraction is delicate rather than robust: the PCF model is fully abstract only after quotienting strategies by intrinsic equivalence, and the quotient is not effective — Loader proved observational equivalence for finitary PCF undecidable, so a fully abstract model yields no decision procedure. Decidability via games survives only in restricted fragments; Ghica and McCusker obtained a regular-language model for second-order Idealized Algol, and decidability fails as the type order rises. Each language feature demands its own relaxation of the innocence, bracketing and visibility conditions together with its own definability proof, so the framework classifies effects without composing them automatically. And strategies are infinite objects: the finite-state presentations that make model checking possible exist only where the type structure is bounded.
© 2026 Lingenic LLC