«

Logic games

By Dmitry Sustretov

(pdf version of this post)

In a recent post, Terence Tao evokes statements that cannot be formalized in first-order logic. David Corfield has left a comment to that post where he mentions “independence-friendly logic”. I thought it was a nice pretext to make a post about evaluation games.

The standard Tarskian definition of truth for first-order formulas is a recursive statement that disassembles a formula down to atomic formulas whose truth can be more or less directly established from the model. Evaluation game is another way to look at this process.

Take a formula, a model and imagine two players, one of which tries to find evidence that the formula is not true in the model and the other tries to prove that the formula is true in the model. By the way, there is a long tradition to call those players \forallbelard (he tries to falsify the formula) and \existsloise (she tries to prove it true) and we will do so too. (I hope you will appreciate how suggestive this notation is after you will have read this paragraph till the end; by the way, these are the names of lovers taken from a medieval story, you might have heard about a poem of Alexander Pope about them). How one would go and set up the rules so that the output of the game would determine the truth of the formula? Instead of giving a rigorous definition, I will give you an example. Let us take the formula

\forall x \forall y \exists z (R(z, x) \land \neg R(z, y))

(this is one of the “extension axioms” of random graphs). We say that logical symbols \land, \forall belong to \forallbelard and \lor, \exists belong to \existsloise. That means that when we encounter a symbol in the formula’s syntactic tree, it is the player that owns that symbol who has a right to make his turn. So, let us start our descent down the tree and first consider \forall x. That means that \forallbelard has to pick an element in the model. \forallbelard wants to make the formula false and he is free to choose the “worst” element possible, to make it harder for \existsloise to prove the formula true. Once he has chosen it, the element is assigned to x. Next, we encounter \forall y and again \forallbelard has the right to assign any element he wants to y. The next time we look at the formula, we see \exists z and that means it’s \existsloise’s turn to assign an element, this time to z. When she does that, she knows what were the elements picked by \forallbelard during two previous turns (sic!), so she can prepare well for the rest of the game.

The last connective — \land — belongs to \forallbelard and is a bit different in a sense that instead of selecting elements in the model, \forallbelard has to select a subformula he wants to evaluate. Notice that \existsloise had better made sure she had chosen an element that makes both subformulas true, because \forallbelard is interested in falsifying the formula and would certainly select the false subformula would such a subformula exist.

We have ended up with an atomic formula (possibly preceded by a negation) and an assignment to its free variables. The rules are simple at that point: if the atomic formula is true in the given model under this assignment, then \existsloise wins, otherwise she loses.

We can now define the truth of a formula (without free variables) as follows: a formula is true in the model iff \existsloise has a winning strategy in this game.

Some technical restrictions apply: the game can only by played on formulas where negations only occur before atomic subformulas. In fact, one can change the game in a way that this restriction is dropped by adding a rule that makes \forallbelard and \existsloise switch roles every time a negation is encountered.

What is good about this definition is that it easily generalises to formulas that contain infinite quantifiers and infinite conjunctions/disjunctions. It is also interesting that little tweaks in the rules of the game lead to different semantics.

Namely, in order to express the formula Terence Tao speaks about

\forall x' \exists y' \forall x \exists y Q(x,y,x',y')

where y depends solely on x (and not on x'), one only has to require that when players make their turns they only know about the last choice made by their opponent.

One can think of many logics (see, for example, David Corfield link to this paper by Samson Abramsky) in terms of game semantics. There is one example that I find particularly elegant: fixed-point logics.

Consider a formula \phi(\bar{x}) in n free variables which contains a n-ary relation symbol R form a distinguished collection of relation symbols. This formula can be seen as an operation on n-ary relations: take a relation S \subseteq M^n, interpret R by S and take the relation defined by \phi(\bar{x}) on M^n as the result of the operation. Let us call this operation \pi_{\phi(\bar{x}), R}: M^n \to M^n. More generally, \phi might have parameters: \phi(\bar{x}, \bar{y}), then the operation that corresponds to parameter values \bar{b} is denoted \pi_{\phi(\bar{x}, \bar{b}), R}. If R occurs positively in \phi (R is preceded by an even number of negations) then the operation is order-preserving and has the least and the greatest fixed points. Fixed-point logics allow to mention fixed points explicitly in a formula. More formally, in addition to usual atomic formulas, one allows atomic formulas of the form LFP_{\bar{x}, R}\phi(\bar{x}, \bar{y}) and GFP_{\bar{x}, R}\phi(\bar{x}, \bar{y}). Their semantics is defined as follows:

M \models LFP_{\bar{x}, R}\phi(\bar{a}, \bar{b}) iff \bar{a} belongs to the least fixed point of \pi_{\phi(\bar{x}, \bar{b}), R}

M \models GFP_{\bar{x}, R}\phi(\bar{a}, \bar{b}) iff \bar{a} belongs to the greatest fixed point of \pi_{\phi(\bar{x}, \bar{b}), R}

For example, consider the natural numbers in the signature with a single function S — the successor function. Then

M \models LFP_{x, P}(x = y \lor \exists z (x = S(z) \land P(z)) iff x \leq y.

Indeed, denote \phi(x,y) \equiv (x = y \lor \exists z (P(z) \land x = S(z)), by Knaster-Tarski theorem the operation \pi_{\phi(x,y), P}^n(\emptyset) becomes stationary on a set X as n goes to infinity, and that X is the least fixed point. Let us find out what is X: we get \{y\} after the first iteration, \{y-1, y\} after the second and so on. This set will become stationary after y steps, it will be \{1, \ldots, y\}. Thus the aforementioned formula really defines x \leq y.

Now let us see how this can be handled with game semantics. We add the following rule: once we encounter a fixed-point atomic formula, we go inside it and continue evaluation game, but when we encounter a distinguished relation symbol, we go back to the root of the last fixed-point formula we entered. One should be careful if with nested fixed-point formulas but I prefer once again wave over the rigorous definition and rather go back to our example. Once the game arrives at the point when \forallbelard had chosen P(z):

LFP_{x, P}(x = y \lor \exists z (x = S(z) \land P(z) \ldots

we must go back to LFP node in the syntactic tree. But this is the same as inserting the whole LFP atomic formula in place of P(z)

LFP_{x, P}(x = y \lor \exists z (x = S(z) \land LFP_{z, P}(z = y \lor \exists z' (x = S(z') \land P(z') \ldots

Since all those LFP are do not longer affect the course of the game I will drop them to ease the reading:

x = y \lor \exists z (x = S(z) \land (z = y \lor \exists z' (z = S(z') \land (z' = y \lor \ldots

Thanks to the rules of the game one can extend the formula in this way infinitely, this will results in the same sequences of turns as the original formula with LFP. As you can see, the fixed point operator turned out to be a means to add a loop operation to the first-order logic and we could make this idea explicit using game semantics.

This entry was posted on September 4, 2007 at 1:55 pm and is filed under Uncategorized. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.

Leave a Reply