Tarski Games.

Rules of Tarski Games. The Tarski game for t.A (or f.B) is played over the judgement tree of t.A (of f.B). There are two players, Eloise and Abelard. The goal of Eloise is to convince Abelard that A is true (that B is false). The goal of Abelard is always the opposite of the goal of Eloise. In t.A, we say that Eloise defends A and Abelard attacks A. In f.B, we say that Eloise attacks B and Abelard defends B.
The positions of the game are all subjudgements of t.A (or f.B). The play starts from the judgement t.A (or f.B). Each player moves from a judgement with his (her) color to some immediate subjudgement. The first player dropping out of the play (because he does not want to move, or he cannot) loses the play.  
A Tarski game for a formula F is a Tarski game for the judgement t.F.

Eloise, according to the definition above,  moves from disjunctive judgments, that is, whenever to accept a judgment requires finding some true immediate subjudgment. For instance, if Eloise moves t.A from t.A∨B, she is trying to convince Abelard of the truth of A∨B by arguing in favor of the truth of A. If Eloise moves f.A from t.A⇒B, she is trying to convince Abelard of the truth of A→B by arguing in favor of the falsity of A (an implication is true when its assumption is false).
  Eloise always loses in the positions t.F, f.T. Indeed, these judgements are disjunctive, she should move, but she cannot, because there are no subjudgements to choose. This corresponds to our idea that t.F, f.T are trivially false. Eloise defends them and loses.  

Abelard, instead, moves from conjunctive judgments, that is, whenever a judgement requires the truth of all its immediate subjudgements. To put otherwise, Abelard moves whenever to reject a judgment requires finding some false immediate subjudgment. For instance, if Abelard moves t.A from t.A∧B, he is trying to convince Eloise of the falsity of A∧B by arguing in favor of the falsity of A. If Abelard moves t.A[t/x] from t.∀x.A, he is trying to convince Eloise of the falsity of ∀x.A by arguing in favor of the falsity of some A[t/x].
  Abelard always loses in the positions t.T, f.F. Indeed, these judgements are conjunctive, he should move, but he cannot, because there are no subjudgements to choose. This corresponds to our idea that t.T, f.F. are trivially true. Abelard attacks them and loses.  

Duality. Whenever we switch t, f we also switch the role of Abelard and Eloise. For instance, in f.∃x.A Abelard tries to convince Eloise of the truth of ∃x.A (the goal of Abelard is the opposite of the goal of Eloise). Therefore Abelard looks for some true example A[t/x], and moves f.A[t/x]. In f.A∨B. Abelard tries to convince Eloise of the truth of A∨B. Therefore Abelard chooses A if he thinks that A is true, and chooses B is he thinks that B is true.
We call this phenomenon "duality".

Created by Mathematica  (October 17, 2006)