§1.1 Introducing Tarski games.

We define a formal language to write the mathematical formulas A about which Eloise and Abelard will discuss. We call a statement of the form: "A is true", "A is false" a judgement: we can identify a formula A with the judgement "A is true". We split judgements into two classes, conjunctive (equivalent to a conjunction of sub-judgements) and disjunctive (equivalent to a disjunction of sub-judgements). We define the rules of the games, expressing the logical arguments Eloise and Abelard can use in favor or against a judgement. We define a tree-like picture of a generic position of a generic play, which we will use to introduce our examples. Eventually, we show by an example that this interpretation of the truth of a mathematical formula is (highly) non-effective.

Created by Mathematica  (October 17, 2006)