1.6  Using Or: Proof by Cases

The previous section met a goal the rules could not reach: from P∨Q, derive Q∨P. The rules could build a disjunction (∨I, Definition 1.5.1), but none of them could use one. This section gives the rule that uses a disjunction, ∨E. It is the most familiar move in mathematics after “suppose”: the split into cases, “if x≥0, then …; if x<0, then …”. It is also the last rule of this chapter. We use it to reach the stalled goal, to prove the laws that let “and” and “or” be rearranged, and to prove three facts about absolute values; the section ends with all the rules of the chapter on one page.

1.6.1. A proof that needs two cases

The absolute value of a real number is defined in two cases: |x|:={xif x≥0,−xif x<0. Suppose we want to prove that |xy|=|x||y| for all real numbers x and y. There is no single computation to do. Which formula gives |xy| depends on the sign of xy, and that depends on the signs of x and y. Yet once the signs are fixed, each case is one line: if x>0 and y<0, for instance, then |xy|=−xy=x⋅(−y)=|x||y|.

So the proof we want has the shape “every real number is ≥0 or <0; in the first case …; in the second case …; so in every case …”. The rules so far cannot say this. The attempt at P∨Q⊢Q∨P in Section 1.5 met the same wall from the other side. It derived that each side of the premise, assumed in a box, leads to the goal: lines 4 and 7 there were P→(Q∨P) and Q→(Q∨P). What it lacked was a rule to say “one of P, Q holds, and either one leads to Q∨P; so Q∨P”: a rule that takes “φ or ψ”, which does not say which side holds, and still reaches a definite conclusion. That is the job of the elimination rule for “or”.

1.6.2. The rule of or-elimination

To use “φ or ψ”, reach your goal from φ, and reach it again from ψ.

The definition block states both rules for disjunction, so that the pair stands in one place: the new rule first, then the two schemas of ∨I recalled from Section 1.5. As in every schema (Definition 1.2.1), the Greek letters stand for arbitrary statements and i,j,k,l,m,n for line numbers.

Definition 1.6.1 (Rules for Disjunction)
iφ∨ψ
jφasm, for ∨E
⋮
kχ
lψasm, for ∨E
⋮
mχ
nχ∨E i, j–k, l–m
iφ
kφ∨ψ∨I i
iφ
kψ∨φ∨I i

The first schema is the rule ∨E (or-elimination, or proof by cases); the other two are ∨I, as in Definition 1.5.1. In ∨E, each line χ (line k and line m) is a line of its box itself, not of a box inside it.

This rule has conditions that matter; read each one.

  • The disjunction. Line i holds a disjunction φ∨ψ, available at line n. The cases are not ours to invent: they are the two sides of a disjunction we already have, as a premise, an assumption, or a line derived earlier. Writing “Case 1 … Case 2 …” does not create it.
  • Two boxes. The first box opens with the left side φ as its assumption, the second with the right side ψ. They are separate: the second opens after the first has closed, and the drawing shows a break in the vertical bar between them. So, by the scope rule of Definition 1.4.2, no line of the second box may cite a line of the first. The disjunction does not tell us which side holds, so we must be ready for both, and each case’s assumption is in force only inside its own box. Each case box’s assumption is printed “asm, for ∨E”; read it as “Case 1: …” and “Case 2: …”.
  • The same last line. Both boxes end in the same statement χ, and in each box χ is a line of that box itself, not of a box opened inside it. The rule then writes χ a third time, outside both boxes, where neither φ nor ψ is assumed. That is honest only because χ was reached whichever case holds.
  • Three citations. The justification “∨E i,j–k,l–m” cites the disjunction first, then the box of the left side, then the box of the right side, each box as a range. Both boxes must be available at line n: closed, and sitting directly in the part of the derivation where line n is (Definition 1.4.2).
  • Any conclusion. The statement χ need not mention φ or ψ. It is whatever we are trying to reach. The next subsection says how to choose it.
Second readingA box of one line

The degenerate case is a box of one line, whose assumption is already χ. Nothing in the rule asks a box to contain more than its assumption, just as nothing in →I did (Example (First boxes)). The second derivation below has two such boxes.

Warning. A case may use only its own assumption. Here is the error in its usual form. Let x be a real number, and split on “x≥0 or x<0”. Case x≥0: then |x|=x. Case x<0: since x≥0, again |x|=x. So |x|=x. The second case cites the assumption of the first, whose box has closed, which the scope rule forbids. The conclusion is false at x=−1.

1.6.3. Cases end in the current goal

Section 1.2 set up two questions: what is the goal’s main connective? and what are the available lines’ main connectives? Section 1.5 answered the first for ∨: postpone a disjunctive goal until one side is in hand. Now we can answer the second. A disjunction on an available line invites ∨E: split on it.

What should the two boxes end in? The rule leaves χ to us, and the choice is always the same. It is the current goal: whatever we are trying to reach at the point where the split is made. That may be the goal of the whole derivation, or a subgoal inside other boxes. The boxes of the split end in it, and the ∨E line that closes the split then writes it outside both boxes, exactly where it was wanted.

Cases end in the current goal.

The two habits fit together. Faced with a goal φ∨ψ and an available disjunction α∨β, do not choose a side of the goal yet: split on α∨β first. Inside each case the current goal is still φ∨ψ, but now a new line is in hand, the case’s assumption, and it may be one side of the goal. Then choose, and the choice may be different in the two boxes. This is exactly how the stalled goal of Section 1.5 goes.

In the Givens/Goal table, each case of a split adds its assumption to the Givens and keeps the same Goal. For the stalled goal:

Givens Goal
P∨Q Q∨P
P∨Q, P (first case) Q∨P
P∨Q, Q (second case) Q∨P
Example (First derivations with “or”)

Show that P∨Q⊢Q∨P, and that P∨P⊢P.

Solution. Idea. For the first: the goal Q∨P is a disjunction, and neither side is in hand, so we postpone it. The premise is a disjunction, so we split on it; the current goal is Q∨P, so both boxes will end there. In the box of P, the right side of the goal is in hand, and ∨I takes it; in the box of Q, the left side is, and ∨I takes that. The choice of side differs between the boxes, and each is safe because it is made inside its own case. The pictures show the two boxes opened, each ending in the goal; then each box filled, with only line 6 left to justify.

1P∨Q
2Pasm, for ∨E
⋮
3Q∨P
4Qasm, for ∨E
⋮
5Q∨P
6Q∨P?
1P∨Q
2Pasm, for ∨E
3Q∨P∨I 2
4Qasm, for ∨E
5Q∨P∨I 4
6Q∨P?
1P∨Q
2Pasm, for ∨E
3Q∨P∨I 2
4Qasm, for ∨E
5Q∨P∨I 4
6Q∨P∨E 1, 2–3, 4–5

The two boxes are separate: the break in the vertical bar between lines 3 and 4 shows where the first closes and the second opens. Line 3 uses the second schema of ∨I (P on the right) and line 5 the first (Q on the left). Both boxes end in Q∨P, and line 6 cites the disjunction on line 1 and the boxes 2–3 and 4–5. Compare the stalled attempt of Section 1.5: its two boxes (2–3 and 5–6 there) are these two boxes, and line 6 here is the step it could not take.

For the second, the goal is P, and the premise is a disjunction, so we split. Both cases are already the goal, so each box consists of its assumption alone.

1P∨P
2Pasm, for ∨E
3Pasm, for ∨E
4P∨E 1, 2–2, 3–3

This is the degenerate case split, in which the two cases are the same case. The box 2–2 is a legal box whose last line is P, a line of that box itself, and so is 3–3.

Second readingOne line short

Change one line of the first derivation and it stops being a derivation. Suppose the second box stops at its assumption Q, and the last line still claims Q∨P:

1P∨Q
2Pasm, for ∨E
3Q∨P∨I 2
4Qasm, for ∨E
5Q∨P∨E 1, 2–3, 4–4

Everything cited exists and is available: the disjunction, a box opened by P, a box opened by Q. What fails is the clause about the last lines. The box 4–4 ends in Q, the box 2–3 ends in Q∨P, and ∨E needs one statement that ends both. The repair is the missing line 5 of the correct derivation.

Quick check. A derivation contains a line P∨Q and a box opened by P that ends in R. No box is opened by Q. Which clause of ∨E stops us writing R? What single change to the derivation would allow it?

Solution. The clause “two boxes”: the rule needs one box opened by each side of the disjunction, and the box opened by Q is missing. Adding a box opened by Q whose last line is R (a derivation of R from Q and the lines available there) allows ∨E, citing the disjunction and both boxes.

Second readingWhy one common last line loses nothing

Why is the rule built like this? Drop the second box, and from “x≥0 or x<0” and a derivation of |x|=x from x≥0 we could conclude |x|=x for every real x, which fails at x=−1. Allow the two boxes to end in different statements χ1 and χ2, and ask what may be written after them: all we honestly know is “χ1 or χ2”. That is already reachable with the rule as it stands, by ∨I at the end of each box, turning both last lines into χ1∨χ2 (exercise B3 carries this out). So the rule asks for one common last line and loses nothing.

The next derivation splits on a disjunction that is not a premise but an assumption, opened because the goal asked for it.

Example (Cases on a hypothesis are two implications)

Show that (P→R)∧(Q→R)⊢(P∨Q)→R.

Solution. Idea. Goal-directed: the goal is an implication, so we open a box with its hypothesis P∨Q, and the current goal inside is R. Premise-directed: the assumption just made is a disjunction, so we split on it, and both case boxes end in the current goal R. In the case P, the premise’s main connective is ∧; ∧E takes out P→R, and →E fires on the case’s assumption. The case Q is the same with the other half of the premise. The pictures show the two case boxes opened, each ending in R; then the first case filled in.

1(P→R)∧(Q→R)
2P∨Qasm, for →I
3Pasm, for ∨E
⋮
5R
6Qasm, for ∨E
⋮
8R
9R∨E 2, 3–5, 6–8
10(P∨Q)→R→I 2–9
1(P→R)∧(Q→R)
2P∨Qasm, for →I
3Pasm, for ∨E
4P→R∧E 1
5R→E 4, 3
6Qasm, for ∨E
⋮
8R
9R∨E 2, 3–5, 6–8
10(P∨Q)→R→I 2–9
1(P→R)∧(Q→R)
2P∨Qasm, for →I
3Pasm, for ∨E
4P→R∧E 1
5R→E 4, 3
6Qasm, for ∨E
7Q→R∧E 1
8R→E 7, 6
9R∨E 2, 3–5, 6–8
10(P∨Q)→R→I 2–9

Line 9 closes the split inside the outer box. It is a line of the outer box itself, so →I at line 10 may cite 2–9. Lines 4 and 7 cite line 1, which lies in no box.

Quick check. In the derivation of Example (Cases on a hypothesis are two implications), which lines and boxes does the ∨E line cite?

Solution. Line 9 cites the disjunction on line 2 and the two case boxes, as ranges: 3–5 and 6–8. All three sit directly in the outer box 2–9, as line 9 does.

Section 1.5 derived the converse, (P∨Q)→R⊢(P→R)∧(Q→R), in Example (A disjunctive hypothesis splits into two implications), using ∨I and no ∨E. So each of the two statements is derivable from the other: cases on a hypothesis are two implications. This is how mathematicians prove “if P or Q, then R”: they prove “if P, then R” and “if Q, then R”. To show that an integer which is one more, or three more, than a multiple of 4 is odd, one treats the two forms separately, and the derivation above is the reason that is enough.

1.6.4. Two cases, two conclusions

When the two cases lead to different statements, each case can still end in the current goal, if the goal is the disjunction of the two.

Example (Constructive dilemma)

Show that (P→R)∧(Q→S), P∨Q⊢R∨S.

Solution. Idea. The goal R∨S is a disjunction with no side in hand: postpone. The premise P∨Q is a disjunction: split, both cases ending in R∨S. In each case ∧E takes out the implication that fits the case, →E fires on the case’s assumption, and ∨I weakens the result to the goal, on the left in one case and on the right in the other. The pictures show the two case boxes opened, each ending in the goal; then the first box filled.

1(P→R)∧(Q→S)
2P∨Q
3Pasm, for ∨E
⋮
6R∨S
7Qasm, for ∨E
⋮
10R∨S
11R∨S?
1(P→R)∧(Q→S)
2P∨Q
3Pasm, for ∨E
4P→R∧E 1
5R→E 4, 3
6R∨S∨I 5
7Qasm, for ∨E
⋮
10R∨S
11R∨S?
1(P→R)∧(Q→S)
2P∨Q
3Pasm, for ∨E
4P→R∧E 1
5R→E 4, 3
6R∨S∨I 5
7Qasm, for ∨E
8Q→S∧E 1
9S→E 8, 7
10R∨S∨I 9
11R∨S∨E 2, 3–6, 7–10

With numbers: let x be a real number with x≥1 or x≤−1. Since x≥1 gives x3≥1, and x≤−1 gives x3≤−1, the derivation shows that x3≥1 or x3≤−1.

The pattern is called the constructive dilemma. When R and S are the same statement there is nothing to weaken: the skeleton of “From a skeleton to a proof about numbers” below reaches R itself.

1.6.5. Laws of “or”

Case splits are not only about numbers. The same two rules prove the laws that let us rearrange “and” and “or”. The first says that “and” distributes over “or”, in both directions.

Proposition 1.6.1 (Distributivity)

P∧(Q∨R)⊢(P∧Q)∨(P∧R), and (P∧Q)∨(P∧R)⊢P∧(Q∨R).

Try it first (ten minutes): derive the first sequent. Which rule will give its last line, and which disjunction will you split on?

Idea. The natural first attempt reads the goal: it is a disjunction, so end with ∨I and aim at one side, say P∧Q. That needs Q on a line, and the premise offers only P and Q∨R; nothing turns Q∨R into Q. The other side fails the same way. So the goal must be postponed, and the attempt shows why: the premise holds a disjunction, Q∨R, and neither of its sides is known. Premise-directed, then: ∧E takes the premise apart into P and Q∨R, and we split on Q∨R, both cases ending in the current goal (P∧Q)∨(P∧R). In the case Q, the side P∧Q is one ∧I away, and ∨I weakens it to the whole goal; the case R builds the other side. In the second sequent the premise itself is the disjunction, so we split on it at once; each case is a conjunction containing P, and ∨I turns its other half into Q∨R.

For the first derivation: the two case boxes opened, each ending in the goal; then lines 5 and 8 written, and only lines 6 and 9 left to justify.

1P∧(Q∨R)
2P∧E 1
3Q∨R∧E 1
4Qasm, for ∨E
⋮
6(P∧Q)∨(P∧R)
7Rasm, for ∨E
⋮
9(P∧Q)∨(P∧R)
10(P∧Q)∨(P∧R)∨E 3, 4–6, 7–9
1P∧(Q∨R)
2P∧E 1
3Q∨R∧E 1
4Qasm, for ∨E
5P∧Q∧I 2, 4
6(P∧Q)∨(P∧R)?
7Rasm, for ∨E
8P∧R∧I 2, 7
9(P∧Q)∨(P∧R)?
10(P∧Q)∨(P∧R)∨E 3, 4–6, 7–9

Before reading on: in the first derivation, which line does each box end on, and why must the two be the same?

Proof. For the first sequent, the following is a derivation with premise P∧(Q∨R) and last line (P∧Q)∨(P∧R).

1P∧(Q∨R)
2P∧E 1
3Q∨R∧E 1
4Qasm, for ∨E
5P∧Q∧I 2, 4
6(P∧Q)∨(P∧R)∨I 5
7Rasm, for ∨E
8P∧R∧I 2, 7
9(P∧Q)∨(P∧R)∨I 8
10(P∧Q)∨(P∧R)∨E 3, 4–6, 7–9

Lines 5 and 8 may cite line 2, which lies in no box and so is available everywhere below it. Both boxes end in the goal, lines 6 and 9, as ∨E at line 10 requires.

For the second sequent, the following is a derivation with premise (P∧Q)∨(P∧R) and last line P∧(Q∨R).

1(P∧Q)∨(P∧R)
2P∧Qasm, for ∨E
3P∧E 2
4Q∧E 2
5Q∨R∨I 4
6P∧(Q∨R)∧I 3, 5
7P∧Rasm, for ∨E
8P∧E 7
9R∧E 7
10Q∨R∨I 9
11P∧(Q∨R)∧I 8, 10
12P∧(Q∨R)∨E 1, 2–6, 7–11

This proves both sequents.

The answer to the prompt: the boxes end on lines 6 and 9, both (P∧Q)∨(P∧R). They must be the same statement because line 10 writes that statement outside both boxes, where neither Q nor R is assumed, and that is honest only if it was reached in each case.

In the second derivation, line 8 derives P a second time instead of citing line 3. It has to: line 3 lies in the box 2–6, which has closed, so line 3 is not available at line 8. Each case must earn its own P.

Second readingDistributivity in words

For a real number x, take P: “x≠0”, Q: “x>0” and R: “x<0”. The first sequent then reads: a non-zero number that is positive or negative is a positive non-zero number or a negative non-zero number. The law is dull in words, which is as it should be. Its use is in derivations, where it moves a case split from inside a conjunction to the outside, and in the laws of sets, where “and” and “or” become intersection and union.

The next derivation shows a case split inside a case: ∨E applied within one box of another ∨E. Before the lines, the shape: each split ends with its own ∨E line, line 11 for the inner split and line 12 for the outer.

1P∨(Q∨R)
2Pasm, for ∨E
⋮
4(P∨Q)∨R
5Q∨Rasm, for ∨E
6Qasm, for ∨E
⋮
8(P∨Q)∨R
9Rasm, for ∨E
⋮
10(P∨Q)∨R
11(P∨Q)∨R∨E
12(P∨Q)∨R∨E

Quick check. In the outline, which line closes the inner split, and which line and boxes does it cite?

Solution. Line 11. It cites the disjunction on line 5 and the boxes 6–8 and 9–10, all of which sit directly in the box 5–11.

Example (Regrouping a disjunction)

Show that P∨(Q∨R)⊢(P∨Q)∨R.

Solution. Idea. The goal is a disjunction, and no side of it is in hand: postpone. The premise is a disjunction: split on it, with both boxes ending in the current goal (P∨Q)∨R. The case P is two weakenings: first to P∨Q, then to the goal. The case Q∨R is itself a disjunction, and neither Q nor R is known; so, inside that box, we split again, and the inner boxes end in the same current goal. In the inner case Q the goal is two weakenings away, and in the inner case R one. The outline above was the first picture; in the second, every box is filled, and only the two ∨E citations are left.

1P∨(Q∨R)
2Pasm, for ∨E
3P∨Q∨I 2
4(P∨Q)∨R∨I 3
5Q∨Rasm, for ∨E
6Qasm, for ∨E
7P∨Q∨I 6
8(P∨Q)∨R∨I 7
9Rasm, for ∨E
10(P∨Q)∨R∨I 9
11(P∨Q)∨R∨E
12(P∨Q)∨R∨E

Before reading on: which disjunction does the inner ∨E cite, and which box must contain it?

1P∨(Q∨R)
2Pasm, for ∨E
3P∨Q∨I 2
4(P∨Q)∨R∨I 3
5Q∨Rasm, for ∨E
6Qasm, for ∨E
7P∨Q∨I 6
8(P∨Q)∨R∨I 7
9Rasm, for ∨E
10(P∨Q)∨R∨I 9
11(P∨Q)∨R∨E 5, 6–8, 9–10
12(P∨Q)∨R∨E 1, 2–4, 5–11

Line 11 is the inner case split. It cites the disjunction on line 5, the assumption of the outer box it sits in, and the boxes 6–8 and 9–10, all of which sit inside the box 5–11, as line 11 does. Line 12 is the outer case split. Line 11 is the inner split’s own ∨E line, so the box 5–11 ends on a line of its own, as Definition 1.6.1 requires.

1.6.6. From a skeleton to a proof about numbers

Almost every proof by cases in analysis has the same skeleton. A known fact supplies the cases, and each case is handled by a separate argument, a small lemma that turns the case’s assumption into the goal. As a derivation, with the fact and the two lemmas as premises:

1P∨Q
2P→R
3Q→R
4Pasm, for ∨E
5R→E 2, 4
6Qasm, for ∨E
7R→E 3, 6
8R∨E 1, 4–5, 6–7

The idea behind it is the whole method of this section at its simplest. The goal R is atomic, so the goal suggests nothing. Premise-directed, the disjunction on line 1 is split, both boxes ending in the current goal R. In each box the matching lemma fires on the case’s assumption. (Example (Cases on a hypothesis are two implications) did the same with the two lemmas packed into one conjunction, and inside a box.)

In a proof about real numbers, the disjunction is usually a fact about the order. The facts about ≤ and the absolute value used below are school algebra: every real number a satisfies a≥0 or a<0; the rules of signs for products; adding two inequalities of the same direction. Here we take them as known. In the language of this chapter, “every real number a satisfies a≥0 or a<0” is a supply of disjunctions: for each number we meet, it gives a line (a≥0)∨(a<0) that ∨E may cite.

The first example is the smallest, and it is written twice: as a proof in which every step carries its rule in brackets, and as a derivation.

Example (A number is at most its absolute value)

Let x be a real number. Prove that |x|≥x, by cases, labeling each step with its rule.

Solution. The goal |x|≥x is the disjunction (|x|>x)∨(|x|=x), and neither side is known for every x (the first fails at x=1, the second at x=−1), so we postpone it. The fact “x≥0 or x<0” is a disjunction to split on. In prose:

We have x≥0 or x<0, and we argue by cases [∨E].

Case x≥0. By the definition of the absolute value, |x|=x [→E]. So |x|≥x [∨I].

Case x<0. By the definition, |x|=−x, and −x>0>x; so |x|>x [→E], which is the school-algebra fact “if x<0, then |x|>x” used on the case’s assumption. So |x|≥x [∨I].

In either case |x|≥x, so |x|≥x.

As a derivation, with the order fact, the definition’s first clause, and the school-algebra fact about negative numbers as premises, and with |x|≥x written out:

1x≥0∨x<0
2x≥0→|x|=x
3x<0→|x|>x
4x≥0asm, for ∨E
5|x|=x→E 2, 4
6|x|>x∨|x|=x∨I 5
7x<0asm, for ∨E
8|x|>x→E 3, 7
9|x|>x∨|x|=x∨I 8
10|x|>x∨|x|=x∨E 1, 4–6, 7–9

It is the skeleton above, with a weakening at the end of each box: line 6 takes the right side of the goal (second schema of ∨I) and line 9 the left side (first schema). Each case took the side it had in hand. At x=3, the first case applies and line 6 reads 3>3 or 3=3; at x=−2, the second applies and line 8 reads 2>−2.

Quick check. In the derivation of Example (A number is at most its absolute value), which statement do lines 6 and 9 both write, and why must they agree?

Solution. Both write (|x|>x)∨(|x|=x), the current goal written out. They must agree because ∨E closes a split only when both case boxes end in the same statement.

The next two examples are longer, and in each the case split is doing real work.

Example (The absolute value of a product)

Let x and y be real numbers. Prove that |xy|=|x||y|.

Solution. We use that |a|=−a whenever a≤0: for a<0 this is the definition, and for a=0 both sides are 0.

The number x satisfies x≥0 or x<0, and we argue by cases [∨E]. Inside each case, y≥0 or y<0, and we argue by cases again.

Case x≥0, y≥0. Then xy≥0, so |xy|=xy=|x||y|.

Case x≥0, y<0. Then xy≤0, so |xy|=−xy=x⋅(−y)=|x||y|.

Case x<0, y≥0. Then xy≤0, so |xy|=−xy=(−x)⋅y=|x||y|.

Case x<0, y<0. Then xy>0, so |xy|=xy=(−x)(−y)=|x||y|.

Each inner case split reaches |xy|=|x||y|, so each outer case does, and hence the equation holds.

The structure is two uses of ∨E, one inside each box of the other: two outer boxes (the sign of x), each containing two inner boxes (the sign of y), and every one of the four inner boxes ending in the same equation, the current goal. The second and third cases needed the remark about a≤0. When x=0 and y<0, the product is 0, not negative, and without the remark the case would have a hole at exactly that point.

A case split need not be the obvious one. The triangle inequality has an equally short proof with two cases, if we split on the sign of the right quantity.

Example (The triangle inequality by cases)

Let x and y be real numbers. Prove that |x+y|≤|x|+|y|.

Solution. First, every real number a satisfies a≤|a| and −a≤|a|. This is itself a proof by cases [∨E]: if a≥0, then |a|=a, so a≤|a|, and −a≤0≤a=|a|; if a<0, then |a|=−a, so −a≤|a|, and a<0<−a=|a|.

Now x+y≥0 or x+y<0, and we argue by cases [∨E].

Case x+y≥0. Then |x+y|=x+y≤|x|+|y|, adding x≤|x| and y≤|y|.

Case x+y<0. Then |x+y|=−x−y=(−x)+(−y)≤|x|+|y|, adding −x≤|x| and −y≤|y|.

Both cases reach |x+y|≤|x|+|y|, so it holds.

Two case splits appear here, one after the other rather than one inside the other. The first proves a small lemma for an arbitrary number a, both halves at once, and its first half, a≤|a|, is Example (A number is at most its absolute value) again. The second uses both halves of the lemma, for a=x and for a=y. Splitting on the sign of x+y instead of the signs of x and y is what saves two cases: the absolute value in the goal is |x+y|, and its sign is the only one the goal’s left side cares about.

Warning. A case split must cover every possibility. A common faulty proof of the triangle inequality treats “x≥0 and y≥0” and “x<0 and y<0”, checks both, and stops. The disjunction of these two cases is not a fact: x=1, y=−1 satisfies neither. So there is no line φ∨ψ for ∨E to cite, and the rule was never legally applied. The missing mixed-sign cases are the interesting ones: at x=1, y=−1 the inequality reads 0≤2, and it is strict.

Warning. Cases must exhaust, and a split that silently drops a value is a missing case in disguise. “Every real x satisfies x>0 or x<0” is false: x=0 satisfies neither. A proof that splits into x>0 and x<0 cites a disjunction that is not available, and proves nothing about x=0. The true disjunctions are “x≥0 or x<0”, and “x>0, or x=0, or x<0”.

Cases may overlap, however. “x≥0 or x≤0” is true for every real x, and x=0 lies in both cases. Nothing in ∨E forbids this: the rule asks that the goal be reached in each case, not that the cases be disjoint. (This is the inclusive “or” of Section 1.1.)

Warning. Because “or” is inclusive, knowing one side of a disjunction says nothing about the other. The form “from P∨Q and P, conclude ¬Q” is called affirming a disjunct, and it is bad. Let n be an integer, with P: “n is even”, Q: “n is a multiple of 3”; at n=6 both premises are true and ¬Q is false. No step of ∨E does this: its cases end in one common statement, never in the falsity of a side.

Quick check. Each of the following begins a proof that x2≥0 for every real number x. Which case splits are exhaustive, so that ∨E may be applied?

  • (i) Case x≥0; case x<0.
  • (ii) Case x>0; case x<0.
  • (iii) Case x≥0; case x≤0.

Solution.

  • (i) Exhaustive: every real number is ≥0 or <0. (ii) Not exhaustive: x=0 is in neither case, so the disjunction cited is false. The claim is still true at 0, but this split never proves it there. (iii) Exhaustive. The cases overlap at x=0, which does no harm: x2=0≥0 is reached in both.

1.6.7. The rules of this chapter

First, as for each rule before it, the newest rule matched against statements larger than single letters.

Example (Instances of ∨E)
Disjunction First box Second box New line
(P∧Q)∨(P∧R) P∧Q … P∨S P∧R … P∨S P∨S
(P→Q)∨(R∧S) P→Q … (R∧S)∨(P→Q) R∧S … (R∧S)∨(P→Q) (R∧S)∨(P→Q)
(P∨Q)∨(Q∧S) P∨Q (a box of one line) Q∧S … P∨Q P∨Q

Not an instance. From (P∨Q)∧R, two boxes opened by P and by Q cannot be closed by ∨E citing that line: its main connective is ∧, so it is no disjunction. Take out P∨Q by ∧E first, and split on that line.

This chapter has introduced six rules, one or two at a time, and the structural clause R. Here is the whole chapter on one page.

Rule Shape You write Lean
∧I φ, ψ ⟹ φ∧ψ “We show P, and we show Q.” constructor
∧E φ∧ψ ⟹ φ (or ψ) “In particular, P.” h.1 (and h.2)
→E φ→ψ, φ ⟹ ψ “Since P implies Q, and P holds, Q.” exact h hp
→I box φ … ψ ⟹ φ→ψ “Assume P. … Hence Q.” intro hp
R φ (available) ⟹ φ, copied “As shown above, P.” exact hp
∨I φ ⟹ φ∨ψ (or ψ∨φ) “So P or Q holds.” left (or Or.inl hp); right
∨E φ∨ψ, box φ … χ, box ψ … χ ⟹ χ “Case 1: P. … so R. Case 2: Q. … so R. In either case, R.” Or.elim h (or cases h)

A written proof often drops the first part of the phrase for ∨E, saying “we argue by cases” without naming the disjunction; when that is not a standard fact such as “x≥0 or x<0”, ask for it, since it is the line the rule cites first. Nothing depends on the Lean column.

Warning (Not allowed: ∨E). Each step breaks the clause of the rule named after it.

  • “Close the split with one case box”: the clause “Two boxes”.
  • “Close it when the boxes end in R and in S”: the clause “The same last line”.
  • “In the second box, cite a line of the first”: the clause “Two boxes” and the scope rule; the boxes are separate (the warning after the rule).
  • “Split on ‘case x>0, case x<0’”: the clause “The disjunction”; the cases must be the sides of an available disjunction, and (x>0)∨(x<0) is not one (the warning on exhaustive cases).
  • “Cite the boxes’ lines one by one”: the clause “Three citations”; each box is cited as a range.

Here is the third step as a derivation, wrong on the left and right on the right, with premises (P∧Q)∨R and R→Q and goal Q.

1(P∧Q)∨R
2R→Q
3P∧Qasm, for ∨E
4Q∧E 3
5Rasm, for ∨E
6Q∧E 3
7Q∨E 1, 3–4, 5–6
1(P∧Q)∨R
2R→Q
3P∧Qasm, for ∨E
4Q∧E 3
5Rasm, for ∨E
6Q→E 2, 5
7Q∨E 1, 3–4, 5–6

The wrong line 6 uses the first case’s assumption in the second case. Its lines never cite premise 2, so they would “derive” Q from (P∧Q)∨R alone, and that claim breaks: with P: “x>0”, Q: “x>1”, R: “x<0”, at x=−1 the premise is true and Q is false.

Here are the rules as schemas. Letters in the number column stand for line numbers; every cited line must be available (Definition 1.4.2), and each box rule needs the box’s last line as a line of that box itself.

Conjunction (Definition 1.2.5): ∧I, and the two forms of ∧E.

iφ
jψ
kφ∧ψ∧I i, j
iφ∧ψ
kφ∧E i
iφ∧ψ
kψ∧E i

Implication (Definition 1.4.1): →E and →I; and repetition, clause (D3) of Definition 1.4.2.

iφ→ψ
jφ
kψ→E i, j
iφasm, for →I
⋮
jψ
kφ→ψ→I i–j
iφ
⋮
kφR i

Disjunction (Definition 1.6.1): the two forms of ∨I, and ∨E.

iφ
kφ∨ψ∨I i
iφ
kψ∨φ∨I i
iφ∨ψ
jφasm, for ∨E
⋮
kχ
lψasm, for ∨E
⋮
mχ
nχ∨E i, j–k, l–m

Each rule is also a move in the search for a derivation. Read by the goal’s main connective, the introduction rules say how a goal is built: that is the move read the skeleton off the goal. Read by an available line’s main connective, the elimination rules say how that line is used: use a premise by its main connective.

Main connective As the goal (goal-directed) As an available line (premise-directed)
∧ two subgoals, one per side; finish with ∧I take it apart with ∧E
→ open a box with the hypothesis; the new goal is the conclusion; close with →I fire it with →E once its hypothesis is on a line, or make the hypothesis a subgoal
∨ postpone; choose a side with ∨I when that side is in hand split with ∨E; both boxes end in the current goal

The table of moves as an order in which to try them:

Diagram. Labels: no, the current goal and the lines in hand, is the goal on an\available line?, is the goal\a wedge or a to ?, is the goal a vee \with a side in hand?, does wedgeE or to E\give a new line?, is an unsplit vee \available ?, stop and try to break the claim, done: cite it,\or copy it by R, build it: wedgeI (two subgoals)\or to I (a box), veeI with that side, write it, veeE : both boxes\end in the goal

The chart uses only this chapter’s rules, and following it never writes an illegal line. It is a guide, not a rule: after asking whether the goal is already in hand, it reads the table’s goal column and then its premise column, each from the top, except that it leaves out two moves. When an available implication ends in the goal but its hypothesis is on no line, make the hypothesis the current goal and start the chart again; items 3, 8 and 10 of Exercise (B7: Fifteen standard sequents) need this. When the goal is a disjunction and neither side is in hand, make one side the current goal; item 14 of Exercise (B7: Fifteen standard sequents) does this in each case. (“Unsplit” at the test for ∨ means not already split by a case box you are inside; without that word the chart would split P∨Q again in each case of item 14 and never stop.) So when the chart stops, try these moves. A claim the chart cannot finish may still be derivable: stopping is no evidence that the claim breaks.

Named moves

  • Try to break it. To test a form, put statements in for the letters that make every premise true and the conclusion false; one such choice shows the form is bad. (Section 1.1)
  • Two ways to attack an argument. Show a premise false, or show a step’s form bad; the two attacks are independent. (Section 1.1)
  • Read the skeleton off the goal. The goal’s main connective chooses the introduction rule: ∧ gives two subgoals, → a box, ∨ a choice to postpone. (Section 1.2)
  • Use a premise by its main connective. Its elimination rule says what you may do with it: take a conjunction apart, feed an implication its hypothesis, split a disjunction into cases. (Section 1.2)
  • Open a box, close a box. An assumption lives exactly as long as its box. (Section 1.4)
  • Work from both ends. Premises at the top, the goal at the bottom; fill the gap from both sides. (Section 1.2)
  • Postpone a disjunction. Choose a side of a goal P∨Q only when that side is in hand. (Section 1.5)
  • Cases end in the current goal. Both boxes of ∨E close on the statement you are trying to reach. (Section 1.6)

Remark (Looking ahead). The rules for “not”, for ⊥, and for “if and only if”, and the rule for proof by contradiction, are the subject of Chapter 2; the method that turns the table of moves above into a way of finding derivations is the subject of Chapter 3.

1.6.8. Exercises

A. Check your understanding

Exercise (A1)
  • (a) State the rule ∨E as a schema, and name the three things its justification cites.

  • (b) For each sentence, taken from a proof, name the disjunction that supplies the cases and the statement both cases end in.

    • “If n is even, then n2+n=n(n+1) is even; if n is odd, then n+1 is even and so is n(n+1). Either way, n2+n is even.”
    • “Both possibilities for the sign of t give t2≥0.”
  • (c) Let n be an integer. True or false, with a reason: “If n is even, then n2 is even. Since every integer is even or odd, n2 is even” is a correct proof by cases that n2 is even.

  • (d) The following is offered as a derivation of P∨Q,P→R⊢R. Name the line that is not justified and the clause of Definition 1.6.1 it violates.

    1P∨Q
    2P→R
    3Pasm, for ∨E
    4R→E 2, 3
    5R∨E 1, 3–4
  • (e) In the first derivation of Proposition 1.6.1, which line is the disjunction that ∨E cites at line 10, and where did it come from? Why does each box end in (P∧Q)∨(P∧R) rather than in P∧Q and P∧R?

  • (f) In the same derivation, why does line 6 use ∨I to put P∧Q on the left? Could line 6 have been (P∧R)∨(P∧Q)?

Solution.

  • (a) The schema is the first one of Definition 1.6.1: from a line i holding φ∨ψ, a box j–k opened by φ, and a box l–m opened by ψ, each ending in the same statement χ as a line of its own, a line n holding χ. The justification “∨E i,j–k,l–m” cites the disjunction and the two boxes.

  • (b) In the first, the disjunction is “n is even or n is odd”, and both cases end in “n2+n is even”. In the second, it is “t≥0 or t<0” (the sentence does not say it, and a careful reader supplies it), and both cases end in t2≥0.

  • (c) False. The disjunction “n is even or n is odd” does not say which side holds, so ∨E needs a second case, reaching “n2 is even” from “n is odd”, and the argument has none. Here the second case cannot be supplied: at n=1 the number n2=1 is odd, so the claim itself is false.

  • (d) Line 5. ∨E needs two boxes, one opened by each side of the disjunction (the clause “two boxes”); line 5 cites only the box opened by P, and no box opened by Q exists. Nor can a box opened by Q simply be added: nothing available reaches R from Q. In fact the sequent’s form is bad, so no correct argument should be expected to reach R from these premises. Try to break it: for a real number x, take P: “x>1”, Q: “x<1”, R: “x>0”. At x=−1 both premises hold and R does not.

  • (e) Line 3, Q∨R, obtained from the premise by ∧E. Each box must end in the current goal, (P∧Q)∨(P∧R), because line 10 writes one statement, the same one that ends both boxes; boxes ending in P∧Q and P∧R would end in different statements, and ∨E could not be applied to them.

  • (f) Line 6 must be the current goal exactly, since both boxes end in it and line 10 writes it. The goal (P∧Q)∨(P∧R) has P∧Q as its left side, so line 6 uses the first schema of ∨I. The line (P∧R)∨(P∧Q) is also an instance of ∨I on line 5 (the second schema), but it is a different statement: the first box would then end differently from the second, whose last line 9 is (P∧Q)∨(P∧R), and ∨E could not cite both boxes.

Exercise (A2: Drill)

Each part takes a line or two. The parts run from reading a split, through a missing line and a justification column, to whole derivations. Let x be a real number and n an integer.

  • (a) “If x≥0, then |x|2=x2; if x<0, then |x|2=(−x)2=x2. So |x|2=x2.” Name the disjunction that supplies the cases, and the common last line.

  • (b) How many case boxes does the proof of Example (The absolute value of a product) open?

  • (c) Inside a box whose current goal is S, the available line Q∨R is split. What do the two case boxes end in?

  • (d) Line 1 is (P∧Q)∨R; a box 2–4 runs from P∧Q to S∨P, and a box 5–7 from R to S∨P. What does “∨E 1, 2–4, 5–7” write?

  • (e) Line 9 is Q, justified “∨E 2, 3–5, 6–8”, with line 3 P→Q and line 6 R. What are lines 2, 5 and 8?

  • (f) Justify each line: 1 P∨(Q∧R), 2 P→S, 3 R→S, premises; 4 P; 5 S; 6 Q∧R; 7 R; 8 S; 9 S. The boxes are 4–5 and 6–8.

  • (g) Two case boxes end in R∧S and S∧R. May ∨E close the split?

  • (h) Find the illegal line.

    1P∨Q
    2P→R
    3Q→R
    4Pasm, for ∨E
    5R→E 2, 4
    6Qasm, for ∨E
    7R→E 3, 4
    8R∨E 1, 4–5, 6–7
  • (i) Is the split “n>0 or n<0” exhaustive for integers?

  • (j) “Case x≥1: x2≥1. Case x≤−1: x2≥1. So x2≥1 for every real x.” What fails?

  • (k) Line 1 is (P∨Q)→R. A student opens a box with P and a box with Q, each ending in R, and writes “R — ∨E 1, 2–4, 5–7”. Correct?

  • (l) Derive P∨Q⊢Q∨(P∨R).

  • (m) Derive (P∧Q)∨(P∧R)⊢P.

  • (n) Derive P∨Q, Q→P⊢P.

  • (o) Derive (P∧Q)∨(R∧S)⊢Q∨R.

Solution.

  • (a) The disjunction is (x≥0)∨(x<0), and both cases end in |x|2=x2.

  • (b) Six: two for the sign of x, and two inside each of those for the sign of y. (The opening remark that |a|=−a for a≤0 is itself a small split on a<0 or a=0, like the lemma in Example (The triangle inequality by cases); counting its two boxes as well gives eight.)

  • (c) S, the current goal at the point of the split.

  • (d) S∨P, the common last line of the two boxes.

  • (e) Line 2 is (P→Q)∨R, the disjunction whose sides open the boxes at lines 3 and 6; lines 5 and 8 are both Q, the last line of each box.

  • (f) 4 assumption, for ∨E; 5 →E 2, 4; 6 assumption, for ∨E; 7 ∧E 6; 8 →E 3, 7; 9 ∨E 1, 4–5, 6–8.

  • (g) No: both boxes must end in the same statement. Add ∧E and ∧I lines so that both end in the current goal, say R∧S.

  • (h) Line 7. It cites line 4, which lies in the box 4–5, closed before line 7. It should read “→E 3, 6”.

  • (i) No: n=0 is in neither case.

  • (j) The split is not exhaustive: (x≥1)∨(x≤−1) is false at x=0, so ∨E has no disjunction to cite. The conclusion fails there too: 02=0<1.

  • (k) No: the main connective of line 1 is →, so it is no disjunction, and ∨E has nothing to split.

  • (l) Box 2–4: 2 P, assumption, for ∨E; 3 P∨R, ∨I 2; 4 Q∨(P∨R), ∨I 3. Box 5–6: 5 Q, assumption, for ∨E; 6 Q∨(P∨R), ∨I 5. Then 7 Q∨(P∨R), ∨E 1, 2–4, 5–6.

  • (m) Box 2–3: 2 P∧Q, assumption, for ∨E; 3 P, ∧E 2. Box 4–5: 4 P∧R, assumption, for ∨E; 5 P, ∧E 4. Then 6 P, ∨E 1, 2–3, 4–5.

  • (n) Box 3–3: 3 P, assumption, for ∨E, already the goal. Box 4–5: 4 Q, assumption, for ∨E; 5 P, →E 2, 4. Then 6 P, ∨E 1, 3–3, 4–5.

  • (o) Box 2–4: 2 P∧Q, assumption, for ∨E; 3 Q, ∧E 2; 4 Q∨R, ∨I 3. Box 5–7: 5 R∧S, assumption, for ∨E; 6 R, ∧E 5; 7 Q∨R, ∨I 6. Then 8 Q∨R, ∨E 1, 2–4, 5–7.

B. Practice

Exercise (B1: The other distributive law)

Show that (P∨Q)∧(P∨R)⊢P∨(Q∧R).

Hint: after taking the premise apart, you will need a case split inside a case.

Solution. The goal is a disjunction with no side in hand, so we postpone it. The premise gives two disjunctions. Split on P∨Q, both cases ending in the goal. In the case P, the goal is one weakening away. In the case Q, we still lack R, so we split on P∨R inside that box: its case P weakens as before, and its case R combines with Q.

1(P∨Q)∧(P∨R)
2P∨Q∧E 1
3P∨R∧E 1
4Pasm, for ∨E
5P∨(Q∧R)∨I 4
6Qasm, for ∨E
7Pasm, for ∨E
8P∨(Q∧R)∨I 7
9Rasm, for ∨E
10Q∧R∧I 6, 9
11P∨(Q∧R)∨I 10
12P∨(Q∧R)∨E 3, 7–8, 9–11
13P∨(Q∧R)∨E 2, 4–5, 6–12

Line 10 cites line 6, the assumption of the enclosing box, which is still open at line 10. Line 12 cites line 3, which lies in no box. Splitting on P∨R first, with the roles of Q and R exchanged, works equally well.

Exercise (B2: The larger of two numbers)

For real numbers a and b, let max(a,b):=a if a≥b, and max(a,b):=b if a<b. Prove that max(a,b)≥a and max(a,b)≥b. Hence deduce that max(a,b)≥12(a+b): the larger of two numbers is at least their average.

Solution. We have a≥b or a<b, and we argue by cases [∨E]; the current goal is the conjunction “max(a,b)≥a and max(a,b)≥b”.

Case a≥b. Then max(a,b)=a. So max(a,b)≥a, since a=a and ≥ allows equality [∨I]; and max(a,b)=a≥b. So both hold [∧I].

Case a<b. Then max(a,b)=b. So max(a,b)=b>a, which gives max(a,b)≥a [∨I]; and max(a,b)=b≥b [∨I]. So both hold [∧I].

In either case max(a,b)≥a and max(a,b)≥b, so both hold.

Adding the two inequalities gives 2max(a,b)≥a+b, and dividing by 2>0 gives max(a,b)≥12(a+b). For instance, max(3,−5)=3≥−1=12(3+(−5)).

Exercise (B3: Two cases, two conclusions)
  • (a) A search for P∨Q,P→R,Q→(S∧T)⊢R∨T has reached the stage below. Name the move, then complete it.

    1P∨Q
    2P→R
    3Q→(S∧T)
    4Pasm, for ∨E
    ⋮
    6R∨T
    7Qasm, for ∨E
    ⋮
    10R∨T
    11R∨T?
  • (b) Use (a) to prove: for every integer n, n2 is a multiple of 4 or one more than a multiple of 8. You may use that every integer is even or odd, and that k(k+1) is even for every integer k.

Solution.

  • (a) The move is to split on the premise P∨Q, each case ending in the current goal: cases end in the current goal. The goal R∨T is a disjunction with no side in hand, so it is postponed, and line 11 will be ∨E citing line 1 and the two case boxes. In the case P, line 2 fires and ∨I weakens R to the goal. In the case Q, line 3 fires, ∧E takes out T, and ∨I weakens it to the goal on the other side.
    1P∨Q
    2P→R
    3Q→(S∧T)
    4Pasm, for ∨E
    5R→E 2, 4
    6R∨T∨I 5
    7Qasm, for ∨E
    8S∧T→E 3, 7
    9T∧E 8
    10R∨T∨I 9
    11R∨T∨E 1, 4–6, 7–10

    The two boxes reach different statements, R at line 5 and T at line 9, and ∨I turns both into the common last line R∨T.

  • (b) Take P: “n is even”, Q: “n is odd”, R: “n2 is a multiple of 4”, S: “n2 is odd”, T: “n2 is one more than a multiple of 8”. The premise P∨Q is the fact we may use. For P→R: if n=2k for an integer k, then n2=4k2. For Q→(S∧T): if n=2k+1, then n2=4k2+4k+1=4k(k+1)+1, which is odd; and with k(k+1)=2m for an integer m, n2=8m+1. By (a), R∨T. For instance, 62=36=4⋅9, and 72=49=8⋅6+1.
Exercise (B4: The smaller of two numbers)

For real numbers a and b, let max(a,b) be as in Exercise (B2: The larger of two numbers), and let min(a,b):=b if a≥b, and min(a,b):=a if a<b. Prove by cases that min(a,b)=−max(−a,−b).

Solution. We have a≥b or a<b, and we argue by cases [∨E]; the current goal is the equation min(a,b)=−max(−a,−b).

Case a<b. Then min(a,b)=a. Also −a>−b, so −a≥−b [∨I], and by the definition of max, max(−a,−b)=−a. Its negative is a=min(a,b).

Case a≥b. Then min(a,b)=b, and −a≤−b. Written out, as the convention on inequalities of Section 1.5 asks when a case split must see the disjunction, this is (−a<−b)∨(−a=−b), and we split again [∨E].

  • If −a<−b, then max(−a,−b)=−b, whose negative is b=min(a,b).
  • If −a=−b, then −a≥−b [∨I], so max(−a,−b)=−a, whose negative is a; and a=b=min(a,b).

Both inner cases reach the goal, so ∨E closes the inner split; then both outer cases have reached it, and ∨E closes the outer split. Hence min(a,b)=−max(−a,−b).

For instance, at a=3, b=−5: min(3,−5)=−5, and max(−3,5)=5, whose negative is −5. At a=b=2: min(2,2)=2, and max(−2,−2)=−2, whose negative is 2.

Exercise (B5: Derive or break)

For each claim, derive it with the rules of this chapter, or break it by statements about a real number x that make its counterexample set true.

  • (a) P∨Q, R⊢(P∧R)∨Q.
  • (b) (P∨Q)∧(P∨R)⊢P∧(Q∨R).
  • (c) P∨(Q∨R), Q→P⊢P∨R.
  • (d) (P∨Q)→R⊢(P→R)∨(Q→R).
  • (e) (P→R)∨(Q→R)⊢(P∨Q)→R.
  • (f) P∨Q, P→R⊢R∨Q.
  • (g) P∨(Q→R), Q⊢P∨R.
  • (h) P∨(Q→R)⊢(P∨Q)→(P∨R).
  • (i) (P∨Q)→(P∨R)⊢Q→R.

Solution.

  • (a) Derive. Split on line 1; in the case P, build P∧R with the premise R.
    1P∨Q
    2R
    3Pasm, for ∨E
    4P∧R∧I 3, 2
    5(P∧R)∨Q∨I 4
    6Qasm, for ∨E
    7(P∧R)∨Q∨I 6
    8(P∧R)∨Q∨E 1, 3–5, 6–7
  • (b) Break. Take P: “x>5”, Q: “x>0”, R: “x<10”. At x=1, P∨Q and P∨R are true (1>0, 1<10) and P is false, so P∧(Q∨R) is false: the counterexample set (P∨Q)∧(P∨R), ¬(P∧(Q∨R)) is true.

  • (c) Derive, with a split inside a case: the case Q∨R is itself a disjunction.

    1P∨(Q∨R)
    2Q→P
    3Pasm, for ∨E
    4P∨R∨I 3
    5Q∨Rasm, for ∨E
    6Qasm, for ∨E
    7P→E 2, 6
    8P∨R∨I 7
    9Rasm, for ∨E
    10P∨R∨I 9
    11P∨R∨E 5, 6–8, 9–10
    12P∨R∨E 1, 3–4, 5–11
  • (d) Derive. The goal is a disjunction; the left side P→R can be built, as in Example (A disjunctive hypothesis splits into two implications), and ∨I then adds the other side.
    1(P∨Q)→R
    2Pasm, for →I
    3P∨Q∨I 2
    4R→E 1, 3
    5P→R→I 2–4
    6(P→R)∨(Q→R)∨I 5
  • (e) Break. Take P: “x<0”, Q: “x>0”, R: “x>5”. At x=1, P→R is true, since its hypothesis fails, so the premise is true; P∨Q is true and R false, so (P∨Q)→R is false. The counterexample set is true.

  • (f) Derive.

    1P∨Q
    2P→R
    3Pasm, for ∨E
    4R→E 2, 3
    5R∨Q∨I 4
    6Qasm, for ∨E
    7R∨Q∨I 6
    8R∨Q∨E 1, 3–5, 6–7
  • (g) Derive. In the second case the case’s assumption is an implication, and the premise Q fires it.
    1P∨(Q→R)
    2Q
    3Pasm, for ∨E
    4P∨R∨I 3
    5Q→Rasm, for ∨E
    6R→E 5, 2
    7P∨R∨I 6
    8P∨R∨E 1, 3–4, 5–7
  • (h) Derive, with a split inside a case, inside a box. The goal is an implication: open the box of P∨Q. Inside it, split on the premise; in its case Q→R, split again on the box’s assumption P∨Q, which is available there.
1P∨(Q→R)
2P∨Qasm, for →I
3Pasm, for ∨E
4P∨R∨I 3
5Q→Rasm, for ∨E
6Pasm, for ∨E
7P∨R∨I 6
8Qasm, for ∨E
9R→E 5, 8
10P∨R∨I 9
11P∨R∨E 2, 6–7, 8–10
12P∨R∨E 1, 3–4, 5–11
13(P∨Q)→(P∨R)→I 2–12

Line 11 cites line 2, the assumption of the box 2–12, which contains line 11; the boxes 3–4 and 5–11 sit directly in that box, as line 12 does.

  • (i) Break. Take P: “x>0”, Q: “x>1”, R: “x>5”. At x=2, P∨R is true, so the premise (P∨Q)→(P∨R) is true; Q is true and R false, so Q→R is false. The counterexample set is true.

  • (ii) and (e) are converses: the original derives and the converse breaks. (i) is a look-alike that drops the shared P from (h)’s conclusion, and breaks. (b) is a look-alike of Exercise (B1: The other distributive law), with the conclusion’s ∧ and ∨ traded.

Exercise (B6: Translate, then derive)

Translate each argument into a sequent with the letters given, then derive it or break its form.

  • (a) Let n be an integer. n is even or n is odd. If n is even, then n(n+1) is even. If n is odd, then n+1 is even. If n+1 is even, then n(n+1) is even. So n(n+1) is even. Letters: E: “n is even”, O: “n is odd”, F: “n+1 is even”, M: “n(n+1) is even”.
  • (b) Let x be a real number. If x>1, then x2>1. If x<−1, then x2>1. And x2>1. So x>1 or x<−1. Letters: P: “x>1”, Q: “x<−1”, R: “x2>1”. If the form breaks, say whether the conclusion is still true for every x with x2>1, and which premise would repair the argument.

Solution.

  • (a) The sequent is E∨O, E→M, O→F, F→M⊢M. Split on the first premise; in the case O the chain of two implications reaches M.
    1E∨O
    2E→M
    3O→F
    4F→M
    5Easm, for ∨E
    6M→E 2, 5
    7Oasm, for ∨E
    8F→E 3, 7
    9M→E 4, 8
    10M∨E 1, 5–6, 7–9
  • (b) The sequent is P→R, Q→R, R⊢P∨Q, and its form breaks: it affirms the consequent of two implications at once. Keep P and Q, and replace R by “x≠0”. Both implications then hold for every x, and at x=12 the premise R is true and P∨Q is false, so the counterexample set P→R, Q→R, R, ¬(P∨Q) is true.

With the argument’s own content no number breaks it, because x2>1 does imply x>1 or x<−1 (Exercise (B3: Necessary and sufficient, used later), part (c)). Adding that fact as the premise R→(P∨Q) gives a one-step derivation, →E on it and the premise R, and makes the other two premises unnecessary. A true conclusion, a bad form: the argument proves nothing until the missing premise is written.

Exercise (B7: Fifteen standard sequents)

Derive each sequent. They are grouped by the move that does the main work.

Read the skeleton off the goal.

  • 1. Q⊢(P→R)→(P→(Q∧R)).
  • 2. ⊢(P∧Q)→((Q→R)→(R∧P)).
  • 3. (P∨Q)→R⊢P→(S→(R∧P)).
  • 4. P→(Q→R)⊢(S∧P)→(Q→(R∨S)).
  • 5. Q→R⊢P→((P→Q)→(R∧P)).

Use a premise by its main connective.

  • 6. P→(Q∧R)⊢(P∧S)→(R∧S).
  • 7. P∧(Q→R), P→Q⊢R∧P.
  • 8. (P∧Q)→R, P→Q⊢P→R.
  • 9. P→(Q→R), S→Q⊢(P∧S)→R.
  • 10. ((P∧Q)→R)→S, P→T, (T∧Q)→R⊢S.

Cases end in the current goal.

  • 11. (P→Q)∨(Q∧R), P⊢Q.
  • 12. (P→R)∨(Q→R)⊢(P∧Q)→R.
  • 13. (P→Q)∨(P→R)⊢P→(Q∨R).
  • 14. P∨Q, S→(Q→R)⊢(S→(P∧S))∨(S→R).
  • 15. P∨(Q∧R), P→(R∧S)⊢R∧(S∨Q).

Solution. 1. Two arrows at the top of the goal give two nested boxes; inside, R comes by →E and joins the premise.

1Q
2P→Rasm, for →I
3Pasm, for →I
4R→E 2, 3
5Q∧R∧I 1, 4
6P→(Q∧R)→I 3–5
7(P→R)→(P→(Q∧R))→I 2–6

2. No premises: the skeleton of the goal is two boxes, and everything inside comes from their assumptions.

1P∧Qasm, for →I
2Q→Rasm, for →I
3Q∧E 1
4R→E 2, 3
5P∧E 1
6R∧P∧I 4, 5
7(Q→R)→(R∧P)→I 2–6
8(P∧Q)→((Q→R)→(R∧P))→I 1–7

3. Two boxes from the goal; inside, ∨I manufactures the premise’s hypothesis. The assumption S is never cited.

1(P∨Q)→R
2Pasm, for →I
3Sasm, for →I
4P∨Q∨I 2
5R→E 1, 4
6R∧P∧I 5, 2
7S→(R∧P)→I 3–6
8P→(S→(R∧P))→I 2–7

4. Two boxes from the goal; the premise fires on a half of the outer assumption, and the implication it gives fires on the inner one.

1P→(Q→R)
2S∧Pasm, for →I
3Qasm, for →I
4P∧E 2
5Q→R→E 1, 4
6R→E 5, 3
7R∨S∨I 6
8Q→(R∨S)→I 3–7
9(S∧P)→(Q→(R∨S))→I 2–8

5. Two boxes from the goal; the inner assumption fires on the outer one, and the premise on the result.

1Q→R
2Pasm, for →I
3P→Qasm, for →I
4Q→E 3, 2
5R→E 1, 4
6R∧P∧I 5, 2
7(P→Q)→(R∧P)→I 3–6
8P→((P→Q)→(R∧P))→I 2–7

6. One box from the goal; inside, each line is read off a main connective: ∧ is taken apart, → is fired.

1P→(Q∧R)
2P∧Sasm, for →I
3P∧E 2
4Q∧R→E 1, 3
5R∧E 4
6S∧E 2
7R∧S∧I 5, 6
8(P∧S)→(R∧S)→I 2–7

7. No box: the conjunction is taken apart, and its two halves feed the two implications.

1P∧(Q→R)
2P→Q
3P∧E 1
4Q→R∧E 1
5Q→E 2, 3
6R→E 4, 5
7R∧P∧I 6, 3

8. The first premise needs its whole hypothesis P∧Q; the box gives P, and the second premise gives Q.

1(P∧Q)→R
2P→Q
3Pasm, for →I
4Q→E 2, 3
5P∧Q∧I 3, 4
6R→E 1, 5
7P→R→I 3–6

9. Both halves of the assumption are used, one by each premise, and the results meet in a third →E.

1P→(Q→R)
2S→Q
3P∧Sasm, for →I
4P∧E 3
5S∧E 3
6Q→R→E 1, 4
7Q→E 2, 5
8R→E 6, 7
9(P∧S)→R→I 3–8

10. The only line mentioning S is the first premise, whose hypothesis is itself an implication: it becomes a subgoal, proved in a box by the other two premises.

1((P∧Q)→R)→S
2P→T
3(T∧Q)→R
4P∧Qasm, for →I
5P∧E 4
6T→E 2, 5
7Q∧E 4
8T∧Q∧I 6, 7
9R→E 3, 8
10(P∧Q)→R→I 4–9
11S→E 1, 10

11. Split on the first premise; in one case the premise P fires the case’s implication, in the other ∧E finishes.

1(P→Q)∨(Q∧R)
2P
3P→Qasm, for ∨E
4Q→E 3, 2
5Q∧Rasm, for ∨E
6Q∧E 5
7Q∨E 1, 3–4, 5–6

12. A box from the goal, then a split inside it, each case ending in the current goal R.

1(P→R)∨(Q→R)
2P∧Qasm, for →I
3P→Rasm, for ∨E
4P∧E 2
5R→E 3, 4
6Q→Rasm, for ∨E
7Q∧E 2
8R→E 6, 7
9R∨E 1, 3–5, 6–8
10(P∧Q)→R→I 2–9

13. A box from the goal, then a split inside it; the current goal Q∨R is reached from a different side in each case.

1(P→Q)∨(P→R)
2Pasm, for →I
3P→Qasm, for ∨E
4Q→E 3, 2
5Q∨R∨I 4
6P→Rasm, for ∨E
7R→E 6, 2
8Q∨R∨I 7
9Q∨R∨E 1, 3–5, 6–8
10P→(Q∨R)→I 2–9

14. The goal is a disjunction, so no box can be opened first: the split comes first, as in Exercise (B3: Two cases, two conclusions) (a), and each case opens its own →I box. In the case Q, the box’s assumption S is what opens the premise: →E on line 2 needs S, which only the box supplies, and only then does the case’s assumption Q give R.

1P∨Q
2S→(Q→R)
3Pasm, for ∨E
4Sasm, for →I
5P∧S∧I 3, 4
6S→(P∧S)→I 4–5
7(S→(P∧S))∨(S→R)∨I 6
8Qasm, for ∨E
9Sasm, for →I
10Q→R→E 2, 9
11R→E 10, 8
12S→R→I 9–11
13(S→(P∧S))∨(S→R)∨I 12
14(S→(P∧S))∨(S→R)∨E 1, 3–7, 8–13

15. Split on the first premise; each case builds both conjuncts of the goal, and S∨Q is reached from a different side in each.

1P∨(Q∧R)
2P→(R∧S)
3Pasm, for ∨E
4R∧S→E 2, 3
5R∧E 4
6S∧E 4
7S∨Q∨I 6
8R∧(S∨Q)∧I 5, 7
9Q∧Rasm, for ∨E
10Q∧E 9
11R∧E 9
12S∨Q∨I 10
13R∧(S∨Q)∧I 11, 12
14R∧(S∨Q)∨E 1, 3–8, 9–13

C. Going deeper

Exercise (C1: Challenge: The reverse triangle inequality)

Let x and y be real numbers. Prove that ||x|−|y||≤|x−y| by splitting into the two cases |x|≥|y| and |x|<|y|, using in each case the triangle inequality of Example (The triangle inequality by cases). Then explain why these two cases exhaust all possibilities, and why a split on the signs of x and y would need four cases.

Solution (Hint 1). The triangle inequality bounds |u+v|. Write x as a sum of two numbers whose absolute values appear in the goal.

Solution (Hint 2). In the case |x|≥|y|, the left side is |x|−|y|. Start from x=(x−y)+y.

Solution. We use two school facts: for real numbers a, b, either a≥b or a<b; and |−a|=|a| for every real a (if a≥0 then −a≤0, so |−a|=−(−a)=a=|a|, using, as in Example (The absolute value of a product), that |b|=−b whenever b≤0; if a<0 then −a>0, so |−a|=−a=|a|).

By the first fact, |x|≥|y| or |x|<|y|, and we argue by cases [∨E].

Case |x|≥|y|. Then |x|−|y|≥0, so ||x|−|y||=|x|−|y|. By Example (The triangle inequality by cases) applied to the numbers x−y and y, |x|=|(x−y)+y|≤|x−y|+|y|, so |x|−|y|≤|x−y|, which is the goal in this case.

Case |x|<|y|. Then |x|−|y|<0, so ||x|−|y||=|y|−|x|. By Example (The triangle inequality by cases) applied to y−x and x, |y|=|(y−x)+x|≤|y−x|+|x|, so |y|−|x|≤|y−x|=|−(x−y)|=|x−y|.

Both cases reach the goal, which proves the inequality.

The two cases exhaust all possibilities because they are the two sides of the disjunction “a≥b or a<b” with a=|x|, b=|y|, and that disjunction holds for all real numbers. The split was chosen by the goal: the outer absolute value is of |x|−|y|, and its formula depends only on the sign of that difference.

A split on signs would decide |x| and |y| separately: x≥0 or x<0 gives the formula for |x|, and inside each case y≥0 or y<0 gives the formula for |y|. That is a case split inside each box of another, with 2⋅2=4 inner boxes, as in Example (The absolute value of a product). Fewer would not do for that method: with only the sign of x fixed, |y| still has no formula.

Marking scheme. (10 points)

  • 2: states the disjunction |x|≥|y| or |x|<|y| and says it holds for all reals.
  • 3: in the first case, removes the outer absolute value correctly and derives |x|−|y|≤|x−y| from the triangle inequality for (x−y)+y.
  • 3: in the second case, the same with the roles exchanged, including |y−x|=|x−y|.
  • 2: explains the four sign cases as a split inside each case of another.

Fatal errors (0 for the step): using ||x|−|y||=|x|−|y| in both cases; applying the triangle inequality to a difference as if |u−v|≤|u|−|v|. A proof that squares both sides instead, or splits on signs, earns the 6 points of the two middle lines if every case is complete.

Exercise (C2: Find the error)

Here is a proof, by four cases, that |x−y|≤|x|+|y| for all real numbers x and y.

Case 1: x≥0. Then |x|=x.

Case 1a: y≥0. Then |y|=y, and |x−y| is x−y or y−x. Since x−y≤x≤x+y and y−x≤y≤x+y, we get |x−y|≤x+y=|x|+|y|.

Case 1b: y<0. Then |y|=−y, and x−y>0, so |x−y|=x−y=|x|+|y|.

Case 2: x<0. Then |x|=−x.

Case 2a: y≥0. Then |y|=y, and x−y<0, so |x−y|=y−x=|y|+|x|.

Case 2b: y<0. Then |y|=−y. Since x≥0 and y<0, we have x−y>0, so |x−y|=x−y≤|x|+|y|, because x≤|x| and −y=|y|.

All four cases give |x−y|≤|x|+|y|.

  • (a) Is the statement true?
  • (b) Find the line that is not justified, and name the rule whose conditions it breaks.
  • (c) Show with specific numbers that the step fails.
  • (d) Repair Case 2b.

Solution.

  • (a) Yes. For instance, it follows from Example (The triangle inequality by cases) applied to x and −y, since |−y|=|y| (shown in the solution of Exercise (C1: Challenge: The reverse triangle inequality)). So the question is not whether the conclusion holds but whether this argument proves it.

  • (b) The sentence “Since x≥0 and y<0, we have x−y>0” in Case 2b. The assumption x≥0 is the assumption of Case 1. In derivation terms, it opens the first box of the outer ∨E, and Case 2b lies inside the second box, which is opened by x<0. Once the first box has closed, its lines are not available (the scope rule of Definition 1.4.2), so Case 2b may not cite x≥0: the rule broken is ∨E, each of whose boxes may cite only lines available at it by the scope rule: its own assumption, what has been derived inside it, and what was available before the box opened; so nothing from the first box, which has closed. The sentence is the reasoning of Case 1b copied into Case 2b, where its assumption is no longer in force. So the box of Case 2 does not reach the goal from the lines available to it, and the final ∨E has no right to cite it.

  • (c) Take x=−3 and y=−1, which is Case 2b. Then x−y=−2, which is not >0, and |x−y|=2≠−2=x−y. The conclusion of Case 2b still holds here (2≤3+1), but the step used to reach it is false.

  • (d) In Case 2b, x<0 and y<0, so |x|=−x and |y|=−y. The number |x−y| is x−y or y−x. Since x<0, we have x−y<−y=|y|≤|x|+|y|. Since y<0, we have y−x<−x=|x|≤|x|+|y|. So in either case |x−y|≤|x|+|y|, using only the assumptions of Case 2b.

Exercise (C3: Exit check: a distributive law, rule by rule)

Derive (P∧Q)∨(R∧Q)⊢(P∨R)∧Q, naming the rule and the cited lines on every line. Then say which steps would change if the premise were (P∧Q)∨(P∧R) and the goal P∧(Q∨R), and which would stay the same.

Solution. The chart would build the conjunction by ∧I, with subgoals P∨R and Q, and reach each one by splitting the premise; that route works (it is the second route below). Here one split is enough: the premise is a disjunction, so we split on it first and build the whole goal in each case; both cases end in the current goal (P∨R)∧Q. In each case, ∧E takes the assumption apart, ∨I builds P∨R from the side in hand, and ∧I builds the goal.

1(P∧Q)∨(R∧Q)
2P∧Qasm, for ∨E
3P∧E 2
4Q∧E 2
5P∨R∨I 3
6(P∨R)∧Q∧I 5, 4
7R∧Qasm, for ∨E
8R∧E 7
9Q∧E 7
10P∨R∨I 8
11(P∨R)∧Q∧I 10, 9
12(P∨R)∧Q∨E 1, 2–6, 7–11

Line by line: 1 is the premise; 2 is the assumption of the first case; 3 and 4 are ∧E on line 2; 5 is ∨I on line 3, first schema; 6 is ∧I on lines 5 and 4, written with P∨R as the left conjunct; 7 is the assumption of the second case; 8 and 9 are ∧E on line 7; 10 is ∨I on line 8, second schema; 11 is ∧I on lines 10 and 9; 12 is ∨E, citing the disjunction on line 1 and the boxes 2–6 and 7–11, both of which end in the goal as lines of their own. No line of the second box cites the first.

With premise (P∧Q)∨(P∧R) and goal P∧(Q∨R), the shape stays the same: a split on the premise, ∧E twice in each box, one ∨I and one ∧I in each box, and ∨E at the end. What changes is which part is weakened and where it goes. The common conjunct is now P, and the parts that differ between the cases are Q and R; so the ∨I lines build Q∨R (from Q in the first box, first schema; from R in the second, second schema), and the ∧I lines write P as the left conjunct, as in the goal. That derivation is the second one of Proposition 1.6.1.

Marking scheme. (10 points)

  • 2: splits on the premise by ∨E, with two boxes opened by its two sides.
  • 2: in each box, takes the assumption apart by ∧E into both conjuncts.
  • 2: in each box, uses ∨I to build P∨R from the side in hand, with the correct schema.
  • 2: in each box, builds the goal by ∧I, so that both boxes end in the same line, the goal.
  • 2: the ∨E line cites the disjunction and both boxes as ranges, and the final sentences name the changed steps (the ∨I lines, now building Q∨R, and the ∧I lines, now with P on the left).

Fatal errors (0 for the step): a line in one box citing a line of the other box; a conclusion drawn inside one box only and then used outside it.

A second route is also correct: split the premise twice, once ending both boxes in P∨R and once ending both in Q, and then join the two results by ∧I outside every box (14 lines). Its points map as follows: 2 for either split with two boxes opened by the premise’s sides; 2 for the ∧E lines in the boxes; 2 for the ∨I sides; 2 for the final ∧I, with the boxes of each split ending in the same line; 2 for the citations and the final sentences.

Exercise (C4: The second half)

A search for Q∨R, Q→(P→S), R→S⊢P→S has written the premises and opened one box; the rest is blank. The finished derivation has 11 lines. Name the move, then complete it.

1Q∨R
2Q→(P→S)
3R→S
4Pasm, for →I
⋮

Solution (Hint 1). Inside the box, what is the current goal, and which available line is a disjunction?

Solution (Hint 2). Line 5 is Q, the assumption of a first case box opened inside the box of P; like the second case box, it must end in the current goal S.

Solution. The moves are two. First, the box of line 4 was read off the goal: P→S is an implication, so the box opened with P, and its current goal is S; it will be closed by →I. Second, inside it, the available disjunction Q∨R (line 1, in no box, so available inside the box) is split, and both case boxes end in the current goal S. In the case Q, line 2 fires to give P→S, which fires on line 4; in the case R, line 3 fires.

1Q∨R
2Q→(P→S)
3R→S
4Pasm, for →I
5Qasm, for ∨E
6P→S→E 2, 5
7S→E 6, 4
8Rasm, for ∨E
9S→E 3, 8
10S∨E 1, 5–7, 8–9
11P→S→I 4–10

Line 7 cites line 4, the assumption of the outer box, which contains line 7. Line 10 is a line of the box 4–10 itself (the case boxes have closed), so →I may cite that box at line 11. Splitting outside the box instead, with both case boxes ending in P→S, is also a correct derivation of the sequent; it does not complete the lines given, because it would split before line 4, not after.

R. Review

Exercise (R1)

Let f be a function and [a,b] an interval. Take the atomic statements C: “f is continuous on [a,b]”, B: “f is bounded on [a,b]” and I: “f is integrable on [a,b]”; you need not know what the words mean. Translate the argument “If f is continuous on [a,b] and bounded there, then f is integrable on [a,b]. f is bounded on [a,b]. f is continuous on [a,b]. So f is integrable on [a,b] and bounded there.” into a sequent, and derive it.

Solution. The sequent is (C∧B)→I, B, C⊢I∧B: three premises and a conclusion, as in Definition 1.2.4. The goal is a conjunction, so it splits into the subgoals I and B. B is a premise. The only line that mentions I is the first premise, whose hypothesis C∧B is built by ∧I (Definition 1.2.5) from two premises; then →E (Definition 1.3.1) gives I.

1(C∧B)→I
2B
3C
4C∧B∧I 3, 2
5I→E 1, 4
6I∧B∧I 5, 2

Line 4 writes C∧B, with C on the left as in the hypothesis of line 1 (∧I may cite 3, 2 or 2, 3); the hypothesis must match exactly. Line 2 is cited twice, at lines 4 and 6: a line is not used up by being cited.

Exercise (R2)

Show that (P→Q)∧(Q→R), P∧S⊢R∧S, and say in one sentence which step you found by working backwards from the goal.

Solution. Premise-directed, both premises are conjunctions and are taken apart by ∧E (Definition 1.2.5); goal-directed, the goal R∧S splits into R and S, and S is already in hand. For R, work backwards as in Example (Chains of implications): Q→R is available, so Q becomes the subgoal; P→Q is available, so P does; and P is in hand.

1(P→Q)∧(Q→R)
2P∧S
3P→Q∧E 1
4Q→R∧E 1
5P∧E 2
6S∧E 2
7Q→E 3, 5
8R→E 4, 7
9R∧S∧I 8, 6

The chain of lines 7 and 8 was found backwards, from the subgoal R to Q to P, and written forwards.

Exercise (R3)

Is ⊢(P∧(P→Q))→(Q∨R)? Justify your answer.

Solution. Yes. The goal’s main connective is the outer →, so the move is to open a box with its hypothesis P∧(P→Q) (Definition 1.4.1). Inside, the current goal is Q∨R, which we postpone. The assumption is a conjunction, so ∧E gives P and P→Q; →E gives Q; now the left side of the goal is in hand, and ∨I (Definition 1.5.1) takes it.

1P∧(P→Q)asm, for →I
2P∧E 1
3P→Q∧E 1
4Q→E 3, 2
5Q∨R∨I 4
6(P∧(P→Q))→(Q∨R)→I 1–5

The derivation has no premises, so it shows ⊢(P∧(P→Q))→(Q∨R). The look-alike start fails: the statement contains ∨, and one might begin with ∨I on the whole goal. But the goal’s main connective is →, not ∨, so ∨I cannot produce it; and even inside the box, choosing the side R of Q∨R would have left the subgoal R, which nothing supplies; the side Q is the one lines 2–4 supply.