§1.3 Some examples of Tarski games.
We include here some examples of mathematical formula, and for each formula an example of play in the related Tarski game. In all cases, but the last one, Eloise eventually convinces Abelard of the truth of the formula. In the last example, Eloise has a winning strategy because the corresponding formula is true. However, this winning strategy is not computable (it cannot be expressed by a program). Therefore, in the real world, sometimes Eloise can select a wrong move, and sometimes Abelard is able to convince her of the falsity of the formula.
In the next section we will show how modify Tarski games (by adding the possibility of retracting a move finitely many times), in such a way that Eloise has a computable winning strategy even in this case.
Propositional logic.
((A∧B)∨((A∧¬B)∨(¬A∧B))).
Propositional logic.
¬(¬A∨B)).
A first order statement: integers are unbounded.
∀x.∃y.(x<y)
A Tarski game with a winning strategy, but no computable winning strategy:
∀x.∃y.∀z.f(x,y)≤f(x,z)
Created by Mathematica (October 17, 2006)