Tarski Games are a non-effective semantic.

Let t.A (or f.A) be any judgement. A strategy s for a player p (Eloise or Abelard) is a map taking any node belonging to p in the judgement tree for t.A  (or f.A), and returning either a child of the node (i.e., a move of p from the node), or the message ``drop'' (i.e., ``I quit''). A strategy s for player p is winning if player p wins all plays in which he follows the strategy s blindly. A (winning) strategy for p on A is a (winning) strategy for p on t.A.

For instance, if ∀x.∃y.P(x,y) is true, a winning strategy for Eloise on ∀x.∃y.P(x,y) takes any node ∃y.P(a,y) of the judgement tree, and returns a winning move P(a,b), that is, some true instance P(a,b) of ∃y.P(a,y). In other words, a winning strategy for ∀x.∃y.P(x,y) includes some map f taking any a and returning some b = f(a) such that P(a,b) is true. The following result is well-known:

Theorem: Tarski games are a sound and complete interpretation of judgements of L.
A formula or judgement is true  if and only if Eloise   has a winning strategy for the corresponding Tarski game.
A formula or judgement is false if and only if Abelard has a winning strategy for the corresponding Tarski game.

Tarski games are a non-effective interpretation of judgements of L. There are true formulas A of L such that Eloise has some winning strategy for t.A, but no computable winning strategy. For instance, if ∀x.∃y.P(x,y) is true, there is a map f such that P(a,f(a)) is true for all a, but this map f does not need to be computable, if the predicate P is complex enough. From a foundational viewpoint, Tarski games does not always interpret the truth formulas of L as something effectively existing in our world, in which all maps are computable. If we are applied mathematicians, Tarski games have, therefore the following drawback: they cannot be used in applications. Assume we know that ∀x.∃y.P(x,y) is true, and we are looking for a map f such that P(a,f(a)) is true for all a. Then we cannot use Tarski games to provide such f.

At the end of this section, we include a detailed example of a formula valid, on which Eloise has no computable winning strategy:
                the formula ∀x.∃y.∀z.f(x,y)≤f(x,z), for f map over N

Theorem: the only formulas of L for which Eloise has a computable winning strategy are all intuitionistic theorems (with ω-rule) of L. By ``intuitionistic'' we mean: derivable no Excluded Middle, in any form whatsoever, and considering ¬A as an abbreviation of the dual of A, and A→B as an abbreviation of ¬A∨B.

Created by Mathematica  (October 17, 2006)