Eloise and Abelard, conjunctive and disjunctive judgements.

We consider the notion of conjunctive (or Abelard's) and disjunctive (or Eloise's) formulas we considered for Tarski games, with only one difference: A⇒B (constructive implication) is conjunctive, while A⊃B (if) is disjunctive.

Eloise and Abelard. We introduce two individuals, Eloise and Abelard we call players. We divide judgements in disjunctive and conjunctive. We say that disjunctive judgements belongs to Eloise, and conjunctive judgements to Abelard. We draw disjunctive judgements, and everything belonging to Eloise in pink. We draw conjunctive judgements, and everything belonging to Abelard in blue.

Let  a denote any atom≠T. Disjunctive judgements are:

t.a (atom≠T),        t.A∨B,            t.∃x.A,            t.A⊃B
            and
f.T,            f.A∧B,            f.∀x.A            f.¬A        f.A⇒B

Let  a denote any atom≠T. Conjunctive judgements are:

t.T,            t.A∧B,            t.∀x.A            t.¬A        t.A⇒B
            and
f.a (atom≠T),        f.A∨B,            f.∃x.A            f.A⊃B    

Duality. If we switch f, t, then conjunctive judgement become disjunctive, and disjunctive judgement become conjunctive.

Why the names conjunctive and disjunctive? If a judgement is conjunctive, then it is equivalent to the conjunction of its immediate judgments. If a judgement is disjunctive, then it is equivalent to the disjunction of its immediate judgments.For instance, t.A∧B is conjunctive and it is equivalent to the conjunction of t.A, t.B. The judgement t.A∨B is disjunctive and it is equivalent to the disjunction of t.A, t.B. The judgments t.¬A, t.A⇒B have only one subjudgement, therefore it is arbitrary to consider them conjunctive or disjunctive. We consider them conjunctive because we interpret them through a quantification over all possible worlds, therefore as some kind of conjunction. t.A⊃B is only classically equivalent to the disjunction of f.A, t.B.

This is the judgement tree of t.∃x.∀y.P(x,y)⇒∃x.(P(x,b)∧P(x,c)), in which, for simplicity, we draw only one subjudgement for each quantifier, and we cut down the tree to the nodes of the form P(x,y). We colour all nodes in pink and blue.

Created by Mathematica  (November 11, 2006)