A Tarski game with a winning strategy, but no computable winning strategy:
∀x.∃y.∀z.f(x,y)≤f(x,z)

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.

An example of formula having a winning strategy, but no computable winning strategy. For instance, we know that each map f:N→N has a minimum point, which is, by definition, some y such that f(y)≤f(z) for all z.The reason is that {f(z)|z in N} is a non-empty set of N, hence it has a minimum (which is f(y), for some y). y is a minimum point of f. However, we cannot in general compute y out of f, because in order to find y we have to compare the values of all f(z), which are infinitely many, and take the smallest one. There are binary maps f(x,y), such that we cannot compute, in the parameter x, some minimum point m(x) of the unary map z|→f(x,z). This means that the formula

    Min = ∀x.∃y.∀z.f(x,y)≤f(x,z)
    
saying: ``all maps z|→f(x,z) have a minimum point y'' is indeed true. However, there is no computable map m(x) taking x and returning some minimum point y=m(x) of z|→f(x,z), that is, some y such that ∀z.f(x,y)≤f(x,z). The reason is: to compute y=m(x) would require, in general, to compute f(x,z) for all z. A winning strategy for Min requires such a map m(x). This means that no winning strategy for Min is computable. However, there are non-computable winning strategies for Min, defined from non-computable maps m(x).

A sample play for Min. Let us play the Tarski game Min and see what goes wrong. Abelard chooses some x=a and attacks ∃y.∀z.f(a,y)≤f(a,z). Eloise replies by selecting some y=b and defending ∀z.f(a,b)≤f(a,z). This move is winning if and only if b is, indeed, a minimum point of z|→f(a,z). This does not need to be the case, in the real world, because b is not computable out of a. Then Abelard chooses some z=c, and if f(a,c)>f(b,c), he wins the play.

In[369]:=

Out[369]=

Now Eloise knows that y=b was a wrong choice. y=c would have been a better one, because f(b,c) is smaller, hence closer to the minimum value, than f(a,c). Eloise, however, cannot retract a previous move if, later on, she discover the move is wrong. In the next section, we will consider a Game Semantic, BCK-Semantic, in which a player can retract a move if he later finds out a better one. This game semantic provides an effective interpretation of formulas of L. The price is to allow a trial-and-error process, instead of a neat strategy, producing the correct move at the first try.

Created by Mathematica  (October 17, 2006)