Game Theoretic Semantics

If a statement is taken as an assertion, then it may be regarded as a point of contention between two parties. These parties could be considered players of a game, the object of which is to justify or deny the assertion. Following the nomenclature set by romantic logicians, we will call the players Eloise and Abelard. Eloise is trying to establish the assertion, while Abelard is trying to refute it.

While this kind of game goes back to C. S. Peirce, the primary postwar publicist for this approach is Jaakko Hintikka, so we will follow his lead in calling this Game Theoretic Syntax and Semantics.

Game Theoretic Syntax

An assertion about an elementary structure

For each state s, there is a rule of the form

"When in state s, with pebbles p₁, ... on vertices v₁, ... resp., do ...".

The Kinds of Rules

There are three kinds of rules.

(Bookkeeping note: here, v₁´, ... and v₁´´, ... are all variables from v₁, ..., or constants.)

The kinds of rules are:

*. The junctive rules are of the form:

(s; v₁, ..., v_k) :- (s´ v₁´, ..., v_k'´) * (s; v₁´´, ..., v_k'´´), where * is "or" (Eloise chooses a junct to defend) or "and" (Abelard challenges a junct).

Q. The quantitative rules are of the form:

(s; v₁, ..., v_k) :- Qw(s'; v₁´, ..., v_k'´,w), where Q is "there exists" (Eloise pebbles a vertex) or "for all" (Abelard pebbles).

ð. The terminal rules are of the form:

(s; v₁, ..., v_k) :- &neg R(v_1', \ldots, v_{k'}'), where R is a relation symbol.

A Program for Connectivity

Consider the following program.

• First, if x = y, she is done.
• Otherwise, she chooses a sequence of zs, one after another, starting with one adjacent to x and proceeding until she finally chooses a z = y.

So Eloise wins this game on a graph iff that graph is connected.

A Picture of Connectivity

We can draw flowcharts of these games. Here is the flowchart for Connectivity.

Capturing Languages

There are many languages that can be represented by games. We start with a definitively neanderthal fact from Charles S. Peirce.

A Peircean Theorem. A query is First Order expressible iff it can be represented as such a game with no recursive states. (See Risto Hilpinen's article "On C. S. Peirce's Theory ..." in The Monist vol. 62 (1982).)

Then there is a gradual evolution, especially after WW2, with the work of Jaakko Hintikka in philosophy (see his article in van Benthem and ter Meulen's LOGIC AND LANGUAGE), and also the more hardcore work of people like L. Svenonius and R. Vaught (see the article by Phokion Kolaitis in Barwise and Feferman's MODEL-THEORETIC LOGICS.) Finally, we have the cro-magnon result described in Y. Moschovakis's ELEMENTARY INDUCTION ON ABSTRACT STRUCTURES (see also the article he co-wrote with A. Kechris in THE HANDBOOK OF MATHEMATICAL LOGIC.)

Theorem A query is FO + LFP expressible iff it can be represented as such a game, perhaps with recursive states.

Generalizations, variations, relations, etc., of this result have been developed separately or in collaborations. For example (and this is only a small sample):

Topology and similar stuff.

By imposing restrictions on the digraphs/flowcharts of the programs, we can get representation theorems for fragments of FO + LFP. Transitive closure logic, Existential Fixed Point logic, stratified Existential Fixed Point logic, and so on, can all be obtained in this way. By relaxing the syntax on the rules, one can obtain game representations for PSPACE, EXPTIME, etc. These variations are similar to the Linear Logic games developed by Andreas Blass.

Weird quantifiers.

Least fixed point logics with weird quantifiers started at once with P. Aczel's article in Kanger's 3rd Scandinavian Symposium (1975). P. Kolaitis developed the theory further in his paper in the 1980 Kleene symposium. This line of research continues, by such people as L. Hella, J. Vaananen, etc.

Games played on machines.

Perhaps the best known example of this is the alternating turing machine of A. Chandra, D. Kozen, and L. Stockmeyer, described in their paper in J. ACM 28:1 (1981). Since then, a number of machines have been developed, including the small menageries introduced in A. Condon's COMPUTATIONAL MODELS OF GAMES.

Games as processes.

Well, of course, games are processes, in a Kripke (modal logic) sort of way (see, e.g., Goldblatt's book or any of the five gillion other introductory texts). R. Parikh (at CUNY) wrote a series of papers in the 1980s about modal game logics.

Additional gadgets.

As a shameless advertizement, I ask the gentle reader to consider the gadgets introduced in I and C 122:2, (1995). Let's look at a few of them below.

Clocks.

Using various "clocks" for keeping track of how many moves have been made, we could capture FO + IFP or FO + PFP.

Recursive states.

If no recursive states are universal, we get FO + pos EFP (an additional restriction on the conjunctive recursive states gives us FO + pos TC); if none are existential, we get FO + pos UFP. We can get FO + TC by adding the appropriate clock to FO + pos TC games.

Meta-Restrictions.

We can capture the higher types (NPTIME, PSPACE, EXPTIME, etc.) by relaxing restrictions on how many variables a given state has.

Guarded quantification.

One very natural thing to do is to restrict quantification. There are many reasons why we would want to do this:

• Most games restrict the kinds of moves that their markers make: it would make sense if we could explicitly represent these restrictions.
• Database computations could be modelled by logics that could represent pointers. (This was my motivation for getting into this area.)
• Process logics could be more naturally represented by game logics. (This was the original motivation that J. van Benthem et al had in developing guarded logics.
• Too much free time on their hands (this may have been K. Compton's motive in coming up with the beast).

For more on this from my own biased and ignorant perspective, click here.

Bisimulation.

Here, we have two structures, and two players, one (the Spoiler) claiming that the two structures are different, and the other (the Duplicator) claiming that they are similar. When he Spoiler moves in one structure, the Duplicator tries to simulate the move in the other structure. If the Duplicator ever fails, he loses at once; if he never loses, he wins (thus his position is analogous to Abelard's, while the Spoiler's position is analogous to Eloise's). This is the kind of game that most logicians are talking about when they talk about (pebble) games. For more on these games, click here.