Game Semantics - Classical Logic

Classical Logic

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 dominant connective to pick one of its branches; play will then continue in that subformula, with whichever player controls its dominant 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 dominant 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 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.

Actually the formulation described above is due to Jaakko Hintikka's GTS-interpretation. The original version of classical (and intuitionistic) logic of Paul Lorenzen and Kuno Lorenz were not defined in relation to models but with the help 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 transform GTS-winning strategies for classical logic into the dialogical winning strategies and vice-versa.

All of these games are of perfect information; the two players always know the truth values of each primitive, and are aware of all preceding moves in the game.