§0.1 The formulas of the game semantic.

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, and "true", "false" the "sign of the 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 associated to Abelard) and disjunctive (equivalent to a disjunction of sub-judgements, and associated to Eloise). We define a sub-formula relation on formulas, and a sub-judgement relation on judgements. We define a tree-like representations of subformulas and subjudgements.

Created by Mathematica  (October 17, 2006)