Subjudgments.

A subjudgments relation for judgments. A subjudgment of t.A, f.A is a subformula of A, with a sign depending on the sign of A. The left-hand-side of an implication and of a negation are taken with the opposite sign. In all other cases the sign of a subjudgment is the sign of the judgment. The rational is: we choose sign in such a way that any judgment is equivalent either to the conjuction or to the disjunction of its immediated subjudgments. For instance: the subformulas of t.A→B are f.A, t.B, and indeed, "A⇒B is true" is equivalent, in classical logic, to "A is false or B is true". The subformulas of t.A∧B are t.A, t.B, and indeed, "A∧B is true" is equivalent to "A is true and B is true". If we introduce constructive implication A⇒B, we intepret it as ``A→B is necessary'', and we consider A⇒B as the unary conjunction of A→B.

Eloise and Abelard. We introduce two individuals, Eloise and Abelard we call players. We divide judgements in disjunctive and conjunctive judgements. 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    

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

t.T,            t.A∧B,            t.∀x.A            t.¬A
            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 judgment t.¬A has only one subjudgement f.A, therefore it is arbitrary to consider it conjunctive or disjunctive. We consider it conjunctive.

Created by Mathematica  (October 17, 2006)