Disjunction Propositional natural deduction

The next connective for logical treatment is 'either... or...'. The formula p OR q is called the disjunction of p and q, which are known as its disjuncts. It is read as 'Either p or q or both'. This is the "inclusive" reading of disjunction, in contrast to the "exclusive" disjunction 'Either p or q but not both' which we rarely need in logic.

Exclusive disjunction, usually written 'XOR', has important uses in computation, for instance in low-level arithmetic, in cryptography, in random number generation and in computer graphics. For knowledge representation purposes, however, it is generally best to avoid it. Compound formulae such as   p XOR q XOR r   tend not to mean what you (probably) expect!

Both inclusive and exclusive disjunctions are used in ordinary language. When the set menu includes "either an entrée or a dessert", this is intended as a, exclusive choice between the two: if you want both, you have to pay extra. On the other hand, a rule that you can see a movie if you are "over 15 or accompanied by an adult" does not prohibit two adults from seeing it together, so that disjunction is certainly inclusive.

Fairly obviously, an inclusive disjunction is true iff at least one of its disjuncts is true. Notice that we may often be justified in asserting a disjunction without being justified in asserting either disjunct. For example, unless we knew that the roulette wheel was going to stop on either red or black, betting on the outcome would be even less rational than it actually is; but if we thereby knew which colour it would stop on, roulette would be even more boring than it actually is and casino owners would be much poorer than they actually are. In this respect, disjunction contrasts with conjunction, for anyone in a position to assert p and q is in a position to assert p and to assert q.

:   OR Introduction

A ORI A OR B

B ORI A OR B

The rule for introducing 'OR' in proofs follows very easily from inclusiveness. There are two cases of it (see vI) as the disjunction may be derived from either of its two disjuncts. It has no effect on the stock of assumptions in play.

The elimination rule is more complicated. It is best approached by way of an apparently simpler rule corresponding to a valid form of argument, a sort of generalisation of IMPE where there is a choice of antecedents:

p OR q,   p IMP r,   q IMP r   therefore   r

Arguments of this form, often called "argument by cases", are plentiful:

Example 12

Either inflation will rise or output will fall; If inflation rises, the recession will deepen; If output falls, the recession will deepen; Therefore (either way) the recession will deepen.

Example 13

Number x is either odd or even; If x is odd, x2 + x is even; If x is even, x2 + x is even; Therefore x2 + x is even.

In formal notation, the corresponding rule is of course

A OR B		A IMP C		B IMP C
C

Recall that this is the short notation, leaving out the sets of assumptions since these just accumulate on the left in the standard fashion. If we put them back in we get the full version:

X   ⊢   A OR B		Y   ⊢   A IMP C		Z   ⊢   B IMP C
X, Y, Z   ⊢   C

But now notice that by the deduction equivalence the second input line

Y   ⊢   A IMP C

comes to the same thing as

Y, A   ⊢   C.

:   OR Elimination

X   ⊢   A OR B Y, A   ⊢   C Z, B   ⊢   C ORE X, Y, Z   ⊢   C

Similarly, the third input is equivalent to

Z, B   ⊢   C.

Substituting these forms of those two lines gives the official ORE rule as in vE. In the linear proof format, the annotation requires us to cite three line numbers, and to note the two discharged assumption numbers of A and B. In the tree format, there are two sub-derivations both ending in C. In one we may discharge assumptions of A and in the other assumptions of B, since the rule is that C is an immediate consequence of A OR B and the two [sub]derivations of C from A and from B.

ORE does look a bit daunting when first encountered, and is in fact the most complicated of all the rules in our deductive system: it is the only rule with more than two input lines, and the only one to discharge two assumptions at once. The best way to become familiar with it is to step through a few proofs.

:   Proof using ORE

[p]2 p IMP (q OR r) IMPE q IMP r [q]1 IMPE q OR r r [r]1 ORE(1) r IMPI(2) p IMP r

Look at the proof of the sequent

p IMP (q OR r),   q IMP r   ⊢   p IMP r

in vEproof, for example. Notice how the ORE step is an instance of the rule as abstractly stated in vE. The disjunction A OR B referred to in the rule is q OR r in this instance, and the set X is {p, p IMP (q OR r)}. Y is the empty set, and Z is {q IMP r}. In the conclusion of the rule, C is r, and the set of assumptions is X ∪ Y ∪ Z which is {p IMP (q OR r), q IMP r, p}. The two assumptions of A and B (i.e. q and r ) are discharged by the application of ORE, leaving the assumption of p to be discharged later by IMPI.

SP {p AND (q OR r) ⊢ (p AND q) OR (p AND r)} PL {1} {1} {p AND (q OR r)} {A} PL {1} {2} {p} {1 ANDE} PL {1} {3} {q OR r} {1 ANDE} PL {4} {4} {q} {A} PL {1,4} {5} {p AND q} {2, 4 ANDI} PL {1,4} {6} {(p AND q) OR (p AND r)} {5 ORI} PL {7} {7} {r} {A} PL {1,7} {8} {p AND r} {2, 7 ANDI} PL {1,7} {9} {(p AND q) OR (p AND r)} {8 ORI} PL {1} {10} {(p AND q) OR (p AND r)} {3, 6 [4], 9 [7] ORE} EP

:   Distribution of AND over OR

In the proof in dist, X, Y and Z are all the same set {p AND (q OR r)}. The eliminated disjunction is line (3). Lines (4) — (6) constitute one subproof and lines (7) — (9) the other. As usual with ORE, the conclusion C occurs three times depending on three different sets of assumptions.

For the animated version, click here.

For the interactive version, click here.