§2.1 Introducing BCK Games (with irreversible backtracking).

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, using irreversible backtracking, we cannot effectively interpret all proofs of A by winning strategy for the game associated to A.

Created by Mathematica  (October 20, 2006)