2.1  Contradiction: Using a Negation

Chapter 1 gave rules for “and”, “implies”, and “or”, and not one of them mentions “not”. Yet written proofs are full of sentences such as “this is impossible”, “this case cannot occur”, and “which contradicts what we assumed”. This section gives the two rules that use a negation: the first says exactly what a clash between two lines is, and the second says what a clash buys. The rule that proves a negation is the subject of the next section.

2.1.1. A case that cannot occur

Here is Argument A of Section 1.1, told as a proof by cases. Let n be an integer whose square is even. Every integer is even or odd, so there are two cases. If n is even, we are done. If n is odd, then n2 is odd; but n2 is even, and no integer is both, so this case cannot occur. Hence n is even.

Chapter 1 has a rule for a proof by cases: ∨E of Definition 1.6.1. It asks for a disjunction and two boxes, one opened by each disjunct, and both boxes must end on the same line, the goal. In the argument above the goal is “n is even”. The first box reaches it at once. The second box does not reach it at all. It reaches “impossible”, and then simply declares itself finished.

Two things are missing, and no rule of Chapter 1 supplies them.

  • A way to record the impossibility: the lines “n2 is even” and “n2 is odd”, together with “no integer is both”, should produce a line that says “contradiction”.
  • A way to close the impossible box with the goal: from the line “contradiction”, the box should be allowed to write “n is even”, so that both boxes end on the same line and ∨E applies.

Section 1.1 introduced the symbols for both. The connective ¬ forms the negation ¬φ, read “not φ”. The constant ⊥, read “contradiction”, is a statement that is false however things stand. There they were symbols only. The two rules below give them their first uses.

2.1.2. The rules for a clash

The rule for recording a clash has a simple content. The statement ¬φ says that φ fails, so a derivation that has both φ and ¬φ available is working in a situation that cannot occur. The rule writes this down as the line ⊥. A second rule then says what such a line is good for.

A statement and its negation clash; from a clash, anything follows.

Definition 2.1.1 (Rules for Contradiction)
iφ
j¬φ
k⊥¬E i, j
i⊥
kφ⊥E i

The left schema is ¬E (not-elimination): if φ and ¬φ stand on lines i and j available at line k, write ⊥, citing both, the unnegated line first. The right schema is ⊥E (contradiction-elimination, or ex falso): if ⊥ stands on a line i available at line k, write any statement φ, citing line i.

Why may ⊥E write anything? A line ⊥ can stand only where the premises and open assumptions cannot all hold together: a derivation that reaches ⊥ describes a situation that never happens. Nothing said there can ever be caught false, just as a promise whose condition is never met is never broken; the subsection “Vacuous truth” below returns to this.

As in every schema (Definition 1.2.1), φ is one statement, the same wherever it occurs, and i,j,k are line numbers. We read ¬E in four bullets.

  • Two given lines, both available (the scope rule of Definition 1.4.2), in either order on the page.
  • Exactly φ and ¬φ: the second is the first with one ¬ in front of the whole of it, symbol for symbol. “Contradicts it in spirit” is not enough: x<1 and x>1 cannot both hold, but neither is the other’s negation as written (the box below).
  • The citation lists the unnegated line first: “¬E i,j” says that line i is φ.
  • The new line is ⊥ and nothing else; what to do with the clash is the business of ⊥E.

And ⊥E in three.

  • Schema. The right one in the block above.
  • Reading. One available line ⊥, cited alone; write any statement, related to nothing above, a negation or ⊥ itself included.
  • Example. From line 4 ⊥, “⊥E 4” writes R, or ¬R, or x=7.
Second readingWhere a line ⊥ comes from, and why ⊥E is honest

Two more observations complete the reading. First, ⊥E is the elimination rule of ⊥: it says how a line ⊥ is used. There is no introduction rule of its own for ⊥. Other rules can pass a ⊥ along (⊥E may write it again, and →E writes it from φ→⊥ and φ), but each of them (R, ∧E, →E, ∨E, whenever their new line is ⊥) needs ⊥ already written, perhaps inside a longer statement, in a line it uses (∨I can bring ⊥ in, but only inside a disjunction). Unless ⊥ already occurs in a premise or an assumption, the first line of a derivation that is ⊥ itself is written by ¬E: it is the one rule whose new line is always ⊥, from lines in which ⊥ need not occur. So ¬E plays two parts at once: it is the way a negation is used, and it is the way ⊥ is produced.

Second, why is ⊥E honest? A rule should never lead from lines that hold to a line that fails. A line ⊥ can stand only in a part of a derivation where the premises and the open assumptions cannot all hold together, at least when the ⊥ was written by ¬E, from some φ and ¬φ that were both available there; that the rules which only pass a ⊥ along keep this property is part of what Section 1.2’s Looking-ahead box promised for every rule. In such a place there is no situation in which the conclusion of ⊥E would have to be checked, so it cannot be caught failing.

In the Givens/Goal table, ¬E adds ⊥ to the Givens once φ and ¬φ are both there; and with ⊥ among the Givens, ⊥E ticks off any goal.

Quick check. Which of these pairs of lines are, as written, an instance of the given lines of ¬E, and in which order must each be cited? The pairs are (i) Q∧R and ¬(Q∧R); (ii) ¬P and ¬¬P; (iii) P→Q and ¬P→Q.

Solution.

  • (i) Yes, with φ=Q∧R; cite the line Q∧R first. (ii) Yes, with φ=¬P: the second line is ¬(¬P). Cite ¬P first, then ¬¬P. (iii) No. The main connective of ¬P→Q is → (Definition 1.1.2), so it is not a negation at all; the ¬ applies to P alone. The negation of P→Q would be ¬(P→Q).

Remark. Convention: negations of order and equality. For real numbers a and b, exactly one of a<b and a≥b holds. So a≥b says the same as ¬(a<b), and likewise a>b the same as ¬(a≤b), a≤b as ¬(a>b), and a<b as ¬(a≥b); and a≠b means ¬(a=b), by definition. A derivation writes the negation out whenever a rule for “not” must see it (¬E here, and the rule of the next section); otherwise, and in prose, the short forms stay. Together with the box of Section 1.5, which writes a≤b out as (a<b)∨(a=b) when ∨I or ∨E must see the disjunction, this fixes how an inequality looks on a line.

The fact “no integer is both even and odd” is a negation of a conjunction, ¬(E∧O) with E for “n is even” and O for “n is odd”. It clashes only with a line E∧O, which ∧I builds from separate lines E and O.

Quick check. For a real number x, which pairs are a clash as written, once the convention is used? (i) x2<0 and x2≥0; (ii) x=2 and x≠2; (iii) x<1 and x>1.

Solution.

  • (i) Yes: x2≥0 is ¬(x2<0); cite x2<0 first. (ii) Yes: x≠2 is ¬(x=2); cite x=2 first. (iii) No: x>1 is ¬(x≤1), and x<1 is not x≤1. The line x≤1, written out, must first be built by ∨I (drill A2(l)).

Warning. A clash must have the exact shape φ, ¬φ. And some pairs that look opposed do not clash at all: x≥1 and x≤1 both hold at x=1.

Warning. ⊥E does not run backwards. From ⊥ we may write φ, or ¬φ, or anything; but from a line φ alone no rule writes ⊥, unless ⊥ already occurs in it. If it could, the true line x=1 would give ⊥, and then ⊥E would give the false line x=2.

2.1.3. First derivations with a clash

The five examples below grow in difficulty. Each Idea says why each rule was chosen, in the two directions Chapter 1 used: from the goal (what does the goal’s main connective ask for?) and from the premises (what does an available line’s main connective let us do?). This section adds one question to each list. From the goal: when nothing produces the goal, can a clash produce it? From the premises: an available negation ¬φ is used in exactly one way, by ¬E, so it asks for φ.

Example (The first clashes)

Show that (a) ⊥⊢P, and (b) P∧Q, ¬Q⊢R.

Idea.

  • (a) is the rule ⊥E itself, the degenerate case with no clash to find. In (b), the first premise is a conjunction, so the premise-directed move takes it apart by ∧E. Its half Q and the premise ¬Q are exactly a pair φ, ¬φ. The goal R has nothing to do with the premises: no rule builds it from them. Only ⊥E can write it, and ⊥E needs a line ⊥, which the clash supplies.

Snapshots for (b): the goal alone; then the goal handed to ⊥E, with ⊥ as the new goal.

1P∧Q
2¬Q
⋮
5R
1P∧Q
2¬Q
⋮
4⊥
5R⊥E 4

Solution.

  • (a) Two lines: the premise, and one application of ⊥E.
    1⊥
    2P⊥E 1
  • (b) Five lines.
1P∧Q
2¬Q
3Q∧E 1
4⊥¬E 3, 2
5R⊥E 4

Line 4 cites line 3 first because line 3 plays φ and line 2 plays ¬φ, with φ=Q. The half P of the first premise is never used; a derivation need not use every premise (Definition 1.2.3).

The next result is the pattern of (b) with nothing extra around it. We state it as a proposition, because later sections cite it.

Proposition 2.1.1 (Contradictory Premises Prove Anything)

P, ¬P⊢Q.

Idea. The premises are a clash as they stand, so ¬E writes ⊥ at once, and ⊥E writes the goal, which nothing else could produce.

Proof. The derivation

1P
2¬P
3⊥¬E 1, 2
4Q⊥E 3

has premises P and ¬P and last line Q. This proves the proposition.

In the next derivation the clash happens inside a box, and the rule ⊥E writes the box’s goal.

Proposition 2.1.2 (Vacuous Implication)

¬P⊢P→Q.

Idea. The goal is an implication, so the goal-directed move of Chapter 1 (→I, Definition 1.4.1) opens a box with its hypothesis P; the new goal is Q. Nothing available mentions Q, so no rule can build it. But inside the box, the assumption P and the premise ¬P clash, and ⊥E writes the box’s goal Q. This is the section’s goal-directed move: when nothing produces the goal, look for a clash.

Snapshots: the box with its goal Q; then the clash named as the subgoal.

1¬P
2Pasm, for →I
⋮
4Q
5P→Q→I 2–4
1¬P
2Pasm, for →I
⋮
3⊥
4Q⊥E 3
5P→Q→I 2–4

Proof. The derivation

1¬P
2Pasm, for →I
3⊥¬E 2, 1
4Q⊥E 3
5P→Q→I 2–4

has premise ¬P and last line P→Q. Line 3 may cite line 1, which lies in no box. This proves the proposition.

Line 4 is the line that makes the box close properly: →I needs the box to end on Q, as a line of that box itself, and ⊥E put it there.

In the next example no clash is lying about. It has to be made.

Example (Manufacturing the other half of a clash)

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

Idea. As before, the goal P→R opens a box on P, and the new goal R occurs nowhere else, so a clash must write it. Inside the box there is no ¬P to clash with. The only negation available is the premise ¬(P∨Q), and the premise-directed question says what it asks for: the line P∨Q. That line is one ∨I away from the assumption P. So the clash is manufactured: the unnegated half of the premise becomes a subgoal, and ∨I is chosen not because the goal is a disjunction but because the premise’s clash needs one.

Snapshots: the box with its goal R; then the subgoal ⊥, for which the premise asks for P∨Q.

1¬(P∨Q)
2Pasm, for →I
⋮
5R
6P→R→I 2–5
1¬(P∨Q)
2Pasm, for →I
⋮
4⊥
5R⊥E 4
6P→R→I 2–5

Solution. Six lines.

1¬(P∨Q)
2Pasm, for →I
3P∨Q∨I 2
4⊥¬E 3, 1
5R⊥E 4
6P→R→I 2–5

Line 4 cites line 3 as φ and line 1 as ¬φ, with φ=P∨Q. In words: if neither P nor Q holds, then P cannot hold, so an implication with hypothesis P is true whatever its conclusion. The mirror image, with Q as the hypothesis, is exercise B1.

Quick check. Inside the box of P, could ⊥E write R straight from line 2? Which lines must come first?

Solution. No. ⊥E needs a line ⊥, and ⊥ needs the pair P∨Q, ¬(P∨Q): first P∨Q by ∨I 2, then ⊥ by ¬E 3, 1.

The last of these first derivations is the pattern of the opening argument: a case split in which one case is impossible.

Example (An impossible case)

Show that P∨Q, P→R, ¬R⊢Q.

Idea. The goal Q is a letter, so the goal gives no introduction rule to aim at. The premises do: P∨Q is a disjunction, and Chapter 1’s premise-directed move for a disjunction is ∨E, with two boxes that both end in the current goal Q. The box of Q ends as soon as it opens: its assumption is already the goal. The box of P cannot reach Q honestly, because nothing in it produces Q. So we look for a clash: P feeds the premise P→R, and R clashes with ¬R. The box ends on Q by ⊥E. This is the second new move: an impossible case closes itself.

Snapshots: the split set up; then the first box’s goal handed to ⊥E.

1P∨Q
2P→R
3¬R
4Pasm, for ∨E
⋮
7Q
8Qasm, for ∨E
9Q∨E 1, 4–7, 8–8
1P∨Q
2P→R
3¬R
4Pasm, for ∨E
⋮
6⊥
7Q⊥E 6
8Qasm, for ∨E
9Q∨E 1, 4–7, 8–8

Solution. Nine lines.

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

The second box consists of its assumption alone, a one-line box, just as in the derivation of P∨P⊢P in Example (First derivations with “or”): its last line is its first line, and that line is Q, which is what ∨E needs. The two boxes are separate: nothing in the second box could cite lines 4–7.

Look at line 7 of this derivation again. The box of P is a case “that cannot occur”, and line 7 is the sentence “so there is nothing to prove”: the case is closed with whatever the other case reaches. Every proof by cases with an impossible case has this line somewhere, usually unwritten.

Warning. The impossible case must be impossible from what is available in its own box. A clash with a line of a sibling box, or of a box that has already closed, is a scope error (Definition 1.4.2), even when the clash “looks right”. In Example (An impossible case) the clash in the box of P uses line 5, from that box, and the premise on line 3; neither lives in another box. Exercise C2 shows the error and what it can prove.

The moves of this section, in one place. Goal ⊥: find a clash. Look for φ and ¬φ among the available lines; if only ¬φ is there, make φ a subgoal. An impossible case closes itself. In a case split, a case that reaches ⊥ ends by ⊥E on the current goal. The next section adds a way to reach the goal ⊥ deliberately, by assuming something.

2.1.4. How the rules look in a mathematical proof

We can now prove the fact of Argument A in Section 1.1, with every rule named. Three school facts about integers enter as premises. An integer n is even if n=2k for some integer k, and odd if n=2k+1 for some integer k. And:

  • (E1) every integer is even or odd;
  • (E2) no integer is both even and odd;
  • (E3) the square of an odd integer is odd.

The third is a computation. If n=2k+1 for an integer k, then

n2=4k2+4k+1=2(2k2+2k)+1,

and 2k2+2k is an integer, so n2 is odd.

Theorem 2.1.3 (Even Square, Even Number)

Let n be an integer. If n2 is even, then n is even.

Idea. The hypothesis “n2 is even” hands us nothing to compute with: it says n2=2j for some integer j, and no algebra turns that into a statement about n. The word “odd” does hand us something, since n=2k+1 can be squared. So we split on (E1) and show that the odd case is impossible: there (E3) makes n2 odd, which clashes with the hypothesis through (E2). The impossible case then closes itself.

Proof. Suppose n2 is even [assumption for →I]. By (E1), n is even or n is odd, and we argue by cases [∨E].

Case n even. This is the goal.

Case n odd. By (E3), n2 is odd [→E]. So n2 is both even and odd [∧I]; this contradicts (E2) [¬E]. So this case cannot occur, and in it n is even [⊥E].

In both cases n is even [∨E]. This proves that if n2 is even, then n is even [→I].

The logic of the proof fits in a derivation. Write E for “n is even”, O for “n is odd”, S for “n2 is even”, and T for “n2 is odd”. Then (E1) for n is E∨O, (E2) for n2 is ¬(S∧T), and (E3) for n is O→T; these are the premises.

1E∨O
2¬(S∧T)
3O→T
4Sasm, for →I
5Easm, for ∨E
6Oasm, for ∨E
7T→E 3, 6
8S∧T∧I 4, 7
9⊥¬E 8, 2
10E⊥E 9
11E∨E 1, 5–5, 6–10
12S→E→I 4–11

Each line is one sentence of the proof.

Line Sentence of the proof
1–3 (E1) for n, (E2) for n2, (E3) for n
4 Suppose n2 is even.
5 Case n even. (A one-line box: it is the goal.)
6 Case n odd.
7 By (E3), n2 is odd.
8 So n2 is both even and odd,
9 which contradicts (E2).
10 So this case cannot occur, and in it n is even.
11 In both cases n is even.
12 This proves that if n2 is even, then n is even.

Line 8 cites line 4, the assumption of the outer box; it may, since the box 4–11 contains line 8 (Definition 1.4.2). Two steps of the proof are not in the derivation: passing from the facts (E1)–(E3), about every integer, to their instances for this n and this n2, and naming the k of (E3). Both are steps about “every” and “some”, used as ordinary reasoning (the note at the start of this chapter).

Quick check. Which sentence of the proof of Theorem 2.1.3 is the rule ⊥E, and what does it write?

Solution. The sentence “So this case cannot occur, and in it n is even”, line 10 of the derivation. It cites the line ⊥ (line 9) and writes E, “n is even”, which is the goal of the case, so that the box of O ends on the same line as the box of E.

Every rule in this proof is a primitive rule: →I, ∨E, →E, ∧I, ¬E, and ⊥E. The next section uses the theorem twice, to prove that no rational number has square 2. Section 2.3 reads the same proof again with shorter steps, as mathematicians usually write it, “by the contrapositive”.

2.1.5. Vacuous truth

We can now settle the question that makes many readers distrust logic. Is the sentence

if x2<0, then x=7

true, for a real number x? The hypothesis never holds, and the conclusion has nothing to do with it. Everyday intuition is unsure what to say. The rules are not unsure.

Example (An implication with an impossible hypothesis)

Let x be a real number. Show that if x2<0, then x=7.

Idea. The goal is an implication, so open a box with x2<0, aiming at x=7. Nothing produces x=7, so look for a clash: the school fact x2≥0 is ¬(x2<0), which clashes with the assumption. This is exactly the derivation of Proposition 2.1.2, with P read as “x2<0” and Q as “x=7”.

Solution. With the school fact as the premise:

1¬(x2<0)
2x2<0asm, for →I
3⊥¬E 2, 1
4x=7⊥E 3
5x2<0→x=7→I 2–4

In prose: suppose x2<0; this contradicts x2≥0; so this case cannot occur, and in it x=7; hence if x2<0, then x=7.

We wrote out all five lines rather than citing Proposition 2.1.2 as a single step. Using an already proved sequent as one line of a new derivation is a genuine new permission, and Section 2.3 grants it; until then, a derivation repeats the steps.

An implication whose hypothesis cannot hold is called vacuously true. Nothing about it was decided by convention. It is forced by two rules that each look harmless: →I, which proves an implication by assuming its hypothesis, and ⊥E, which closes an impossible case.

Everyday language agrees. A friend says: “if you finish the exercises by Friday, I will buy you lunch”. You do not finish them. Whatever your friend does on Friday, the promise has not been broken. A promise never tested is never broken.

Vacuous truth is not a curiosity; it is what makes case splits work. In Example (An impossible case), line 7 closed the impossible case by ⊥E, and line 10 of the derivation of Theorem 2.1.3 did the same.

Warning. “True” is not “useful”. The statements “if x2<0, then x=7” and “if x2<0, then x≠7” are both true, and neither says anything about x or about 7. Likewise “if n is an even prime greater than 2, then n=17” is true and empty. When a hypothesis turns out to be impossible, suspect the hypothesis; do not believe the conclusion.

2.1.6. Two sequents that sound wrong

Two sequents in hand sound wrong when read aloud with unrelated statements. The first is Q⊢P→Q: a box opened with P, whose only other line repeats Q (line 1 lies in no box), closed by →I, as in Exercise B2 of Section 1.4. The second is ¬P⊢P→Q, Proposition 2.1.2. Read aloud: “7 is odd; so, if every square is negative, then 7 is odd”, and “7 is not even; so, if 7 is even, then every square is negative”. They are called the paradoxes of material implication.

Each comes from a rule, so whoever rejects one must say which rule goes: the first rests on →I closing a box whose assumption no line uses (with R copying a line in from outside), the second on ⊥E. Some logics, built for purposes other than mathematics, do drop ⊥E; this book keeps it, and Exercise B3 of Section 2.5 shows that the classical rule would bring it back anyway. The same rule gives Proposition 2.1.1: from a clash, anything.

Mathematics does not suffer: its “if” almost always sits under “every”, joining two statements about one variable, as in “for every integer n, if n is a multiple of 4, then n is even”. Instances with a false hypothesis (“if 3 is a multiple of 4, then 3 is even”) are true and empty, as the paradoxes say; the content lies where the hypothesis holds, and there the promise is exact. Nobody wants to prove a sentence whose two parts share nothing.

Quick check. Let x be a real number. Which of the two sequents makes “if x2<0, then x>5” true, and which makes “if x<−3, then x2+1>0” true?

Solution. The first by ¬P⊢P→Q, since x2<0 fails (x2≥0 is ¬(x2<0), the convention box); the second by Q⊢P→Q, since x2+1>0 holds whatever x is.

Second readingThe ‘if’ of a counterfactual

“If 7 were even, 7 would be divisible by 2” sounds true, and “if 7 were even, 7 would be divisible by 3” sounds false, though the two share the false hypothesis “7 is even”. By ¬P⊢P→Q, both material implications are true. So the subjunctive “if” of everyday talk is not the connective →: whether it holds depends on more than the truth of its two parts. Mathematics rarely uses it. When a proof says “if n were odd, then n2 would be odd”, it is working inside a box whose assumption is “n is odd”, and its “if” is the material one.

2.1.7. The rule card

Before the card, the two rules at work on large statements, one use per row.

Example (Instances of ¬E and ⊥E)
Rule φ Cited lines New line
¬E P∨(Q∧R) P∨(Q∧R), then ¬(P∨(Q∧R)) ⊥
¬E ¬(P→Q) ¬(P→Q), then ¬¬(P→Q) ⊥
⊥E (P∧Q)→¬R ⊥ (P∧Q)→¬R

Not instances. (i) The lines P→Q and P→¬Q are no pair for ¬E: the second is an implication, not ¬(P→Q), and no single φ makes the two lines φ and ¬φ. (ii) From the line P∧¬P, “Q — ⊥E” is not an instance: ⊥E cites a line that is ⊥ itself. Take P and ¬P out by ∧E, write ⊥ by ¬E, then ⊥E.

Chapter 1’s seven rules are on the card at the end of Section 1.6; here are this chapter’s so far.

Rule Shape You write Lean
¬E φ, ¬φ ⟹ ⊥ “…, which contradicts …” exact hn hp (goal False)
⊥E ⊥ ⟹ any φ “This case cannot occur.” “So there is nothing to prove.” exfalso

In Lean the two steps are often taken together: absurd hp hn closes any goal from a proof hp of P and a proof hn of ¬P, which is ¬E followed by ⊥E, and the tactic contradiction finds such a pair by itself.

Warning (Not allowed: ¬E and ⊥E). Each step breaks the bullet of the rule’s reading named after it.

  • “⊥ from x<1 and x>1, as written”: the lines must be exactly φ and ¬φ (Exactly φ and ¬φ; the convention box, drill A2(l)).
  • “⊥ — ¬E j,i”, with line j the negation: the unnegated line is cited first (The citation).
  • “⊥ from the one line P”: ¬E needs two lines, and ⊥E runs from ⊥, never to it (Two given lines; the warning that ⊥E does not run backwards).

Remark (Looking ahead). Chapter 4 gives each connective a truth table. The rows of → with a false hypothesis are exactly the ones that →I and ⊥E force here.

2.1.8. Exercises

A. Check your understanding

Exercise (A1)
  • (a) Write the schemas of ¬E and ⊥E from memory.
  • (b) Match each sentence, taken from proofs, with the rule it uses, ¬E or ⊥E: “But n was assumed odd, and we have just shown it is even”; “In this case x2<0, which is impossible, so there is nothing to prove”.
  • (c) True or false, with a reason: ⊥E lets us write ⊥ from any line.
  • (d) In Example (An impossible case), why is the second box only one line long?
  • (e) In the derivation after Theorem 2.1.3, why does line 8 need line 4, and why may it cite it?

Solution.

  • (a) ¬E: from a line i with φ and a line j with ¬φ, both available, write ⊥ at line k, citing i,j. ⊥E: from an available line i with ⊥, write any statement φ at line k, citing i. The two schemas are those of Definition 2.1.1.

  • (b) The first is ¬E: “odd” and “even” clash through (E2), and the sentence records the clash. The second is ⊥E: “impossible” records a clash (an ¬E against x2≥0, left unsaid), and “there is nothing to prove” closes the case with whatever the case needs.

  • (c) False. ⊥E runs from ⊥ to any statement, not from any statement to ⊥. ⊥E needs a line ⊥ to start from. The rule that records a clash as ⊥ is ¬E, and it needs two lines φ and ¬φ.

  • (d) The box is opened by Q, and Q is already the goal of both boxes. So the box’s first line is also its last line, which is all ∨E asks of it.

  • (e) Line 8 is S∧T, built by ∧I from S and T; line 4 is the only line that says S. It may cite line 4 because the only box containing line 4, the box 4–11, also contains line 8 (the scope rule of Definition 1.4.2).

Exercise (A2: Drill)

Each part takes a line or two. Lines are numbered as in a derivation. The parts run from one step, through a missing line, a justification column and steps to judge, to short derivations.

  • (a) Lines 1 ¬(P∧Q), 2 P∧Q. What does “¬E 2, 1” write?
  • (b) Lines 1 ¬¬P, 2 ¬P. Which line is φ for ¬E, and how is the step cited?
  • (c) Line 1 is ⊥. Which of P, ¬P, ⊥, x=7 may “⊥E 1” write?
  • (d) Lines 4 (P→Q)∧R and 6 ¬((P→Q)∧R) are available at line 7. Write line 7 by ¬E, with its citation.
  • (e) Line 7 is ⊥, justified “¬E 5, 2”, and line 2 is ¬(Q∨R). What is line 5?
  • (f) Line 9 is ¬P∨R, justified “⊥E 8”. What is line 8?
  • (g) Justify each line, the first three being premises: 1 ¬(P∨Q), 2 R→P, 3 R, 4 P, 5 P∨Q, 6 ⊥, 7 S.
  • (h) Lines 1 ¬P∧Q, 2 P. Is “3. ⊥ — ¬E 2, 1” legal?
  • (i) Line 1 is P. May “2. ⊥ — ⊥E 1” be written?
  • (j) For a real number x, do the lines x≥1 and x≤1 clash?
  • (k) Find the illegal line: 1 P→Q; 2 ¬Q; 3 | P; 4 | Q, →E 1, 3; 5 | ⊥, ¬E 2, 4; 6 | R, ⊥E 5; 7 P→R, →I 3–6.
  • (l) For one real number x, lines 1 x<1 and 2 x>1 are given. Make them a clash, line by line.
  • (m) Derive P, ¬P∧Q⊢R.
  • (n) Derive ¬Q⊢Q→P.
  • (o) Derive P→Q, ¬Q, P⊢R.

Solution.

  • (a) ⊥.

  • (b) φ=¬P (line 2), and ¬φ=¬¬P (line 1): the step is cited “¬E 2, 1”.

  • (c) All four: ⊥E writes any statement.

  • (d) 7 ⊥, “¬E 4, 6”: line 4 is φ, line 6 is ¬φ.

  • (e) Q∨R, the unnegated form of line 2.

  • (f) ⊥: ⊥E cites one line, and it is ⊥.

  • (g) 4 →E 2, 3; 5 ∨I 4; 6 ¬E 5, 1; 7 ⊥E 6.

  • (h) No: line 1’s main connective is ∧, so it is not a negation. First write ¬P by ∧E 1 as line 3, then ⊥ by ¬E 2, 3.

  • (i) No: ⊥E starts from a line ⊥; no rule writes ⊥ from a single line P.

  • (j) No: both hold at x=1.

  • (k) Line 5: the unnegated line comes first. With line 2 as φ, line 4 would have to be ¬¬Q. Correct: “¬E 4, 2”.

  • (l) Write line 2 as ¬((x<1)∨(x=1)) (x>1 says that x≤1 fails, and x≤1 is written out because ∨I must build it); 3 (x<1)∨(x=1), ∨I 1; 4 ⊥, ¬E 3, 2.

  • (m) 3 ¬P, ∧E 2; 4 ⊥, ¬E 1, 3; 5 R, ⊥E 4.

  • (n) 2 | Q, assumption; 3 | ⊥, ¬E 2, 1; 4 | P, ⊥E 3; 5 Q→P, →I 2–4.

  • (o) 4 Q, →E 1, 3; 5 ⊥, ¬E 4, 2; 6 R, ⊥E 5.

B. Practice

Exercise (B1: Two clashes)
  • (a) Show that ¬(P∨Q)⊢Q→R.
  • (b) Show that (P→Q)∧¬Q, P⊢¬R, and say why ⊥E may write a negation.

Solution.

  • (a) As in Example (Manufacturing the other half of a clash), with Q in place of P: the box of Q manufactures P∨Q by ∨I on the other side.
    1¬(P∨Q)
    2Qasm, for →I
    3P∨Q∨I 2
    4⊥¬E 3, 1
    5R⊥E 4
    6Q→R→I 2–5
  • (b) Take the first premise apart, fire the implication on the second premise, and clash.
1(P→Q)∧¬Q
2P
3P→Q∧E 1
4¬Q∧E 1
5Q→E 3, 2
6⊥¬E 5, 4
7¬R⊥E 6

Line 7 is an instance of ⊥E with φ=¬R: the schema allows any statement in place of φ, and a negation is a statement.

Exercise (B2: An even successor)

Let n be an integer. Prove that if n+1 is even, then n is odd, by cases on (E1) with one case shown impossible. Tag each step with its rule, as in the proof of Theorem 2.1.3.

Solution. Suppose n+1 is even [assumption for →I]. By (E1), n is even or n is odd, and we argue by cases [∨E].

Case n even. Write n=2k with k an integer. Then n+1=2k+1, so n+1 is odd, by the definition of odd [→E]. So n+1 is both even and odd [∧I]; this contradicts (E2) [¬E]. So this case cannot occur, and in it n is odd [⊥E].

Case n odd. This is the goal.

In both cases n is odd [∨E]. This proves that if n+1 is even, then n is odd [→I].

The step “n even, so n+1 odd” plays the part that (E3) played in the theorem: it is the implication fired by →E inside the impossible case. Here the impossible case is the first one, and the other case is the goal.

Exercise (B3: Two vacuous promises)

Let x be a real number. Prove that if x2+1≤0, then x>100; and that if x2+1≤0, then x<−100. Write each as a derivation with one premise, a school fact, and explain why the two statements together are no paradox.

Solution. The school fact is x2+1>0, true for every real x since x2≥0 gives x2+1≥1>0. For real numbers, x2+1>0 says the same as ¬(x2+1≤0). The first derivation is the pattern of Example (An implication with an impossible hypothesis):

1¬(x2+1≤0)
2x2+1≤0asm, for →I
3⊥¬E 2, 1
4x>100⊥E 3
5x2+1≤0→x>100→I 2–4

The second is the same, with x<−100 on lines 4 and 5: ⊥E may write any statement.

No real number is both greater than 100 and less than −100. That is no paradox, because neither implication ever applies: its hypothesis holds for no real x. Both are vacuously true, and both say nothing about x, as the warning on vacuous truth says.

Exercise (B4: An impossible case, scaffolded)

A search for P∨Q, P→R, Q→S, ¬R⊢S has reached the stage below. Name the move, then complete it.

1P∨Q
2P→R
3Q→S
4¬R
5Pasm, for ∨E
⋮
8S?
9Qasm, for ∨E
⋮
10S?
11S∨E 1, 5–8, 9–10

Solution. The move is an impossible case closes itself. The case P cannot reach S honestly: nothing in it produces S. So it reaches a clash: P fires line 2, and R clashes with line 4. The case Q reaches S by firing line 3.

1P∨Q
2P→R
3Q→S
4¬R
5Pasm, for ∨E
6R→E 2, 5
7⊥¬E 6, 4
8S⊥E 7
9Qasm, for ∨E
10S→E 3, 9
11S∨E 1, 5–8, 9–10
Exercise (B5: Derive or break)

For each claim, either derive it with the rules of Chapter 1 and of this section (¬E and ⊥E; no other rule for “not” yet), or break it by statements about a real number x that make its counterexample set true at one value of x.

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

Solution.

  • (a) Derive. Split on the first premise; the case P∧¬Q is impossible beside the premise Q, and the case R is the goal.
    1(P∧¬Q)∨R
    2Q
    3P∧¬Qasm, for ∨E
    4¬Q∧E 3
    5⊥¬E 2, 4
    6R⊥E 5
    7Rasm, for ∨E
    8R∨E 1, 3–6, 7–7
  • (b) Break. Take P: “x>0”, Q: “x>5”. At x=1, P∨Q is true (1>0), ¬Q is true (1>5 fails), and P is true, so ¬¬P is true: the counterexample set P∨Q, ¬Q, ¬¬P is true.

  • (c) Derive. The premise P fires the implication, and its conclusion clashes with P.

    1P→¬P
    2P
    3¬P→E 1, 2
    4⊥¬E 2, 3
    5Q⊥E 4
  • (d) Break. Take P: “x>3”, Q: “x>1”. The premise P→Q holds for every x. At x=2, ¬P is true (2>3 fails) and Q is true (2>1), so ¬¬Q is true: the counterexample set P→Q, ¬P, ¬¬Q is true.

  • (e) Derive. The goal is an implication; inside its box, ∧I manufactures the other half of the clash with the first premise.

    1¬(P∧Q)
    2P
    3Qasm, for →I
    4P∧Q∧I 2, 3
    5⊥¬E 4, 1
    6R⊥E 5
    7Q→R→I 3–6
  • (f) Break. Take P: “x>0”, Q: “x>5”. At x=1, P∧Q is false, so ¬(P∧Q) is true; and ¬P and Q are both false, so ¬P∨Q is false. The counterexample set ¬(P∧Q), ¬(¬P∨Q) is true.

  • (g) Break. Take P: “x>5”, Q: “x>0”, R: “x>3”. The premise P→R holds for every x. At x=1, P∨Q is true (1>0), ¬R is true (1>3 fails), and P is false, so ¬P is true: the counterexample set P∨Q, P→R, ¬R, ¬P is true.

  • (h) Derive. Inside the box of P, the first premise fires, and its half ¬R clashes with the premise R.

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

The four that break are look-alikes. (b) draws the wrong conclusion from a refuted disjunct: the disjunctive syllogism of Section 2.3, after putting the disjunction in the other order, gives P, not ¬P. (d) denies the antecedent, the look-alike of the modus tollens that Section 2.3 derives. (g) is a look-alike of Example (An impossible case), whose conclusion is the other disjunct. (f) is a look-alike of a De Morgan law of Section 2.5. The four that derive follow worked patterns of this section: Example (An impossible case) for (a), Proposition 2.1.1 for (c), Proposition 2.1.2 for (e) and (h).

Marking scheme. (16 points) For each claim: 1 for the verdict; 1 for a derivation every line of which checks, or for a choice of statements and one value of x at which every member of the counterexample set is true. Fatal errors (0 for the claim): a “break” at which some premise is false; a derivation that uses a rule not yet available (¬I, RAA or a derived rule of Section 2.3).

Exercise (B6: Name the rule you reject)
  • (a) List the rules used by a derivation of ¬P⊢P→Q and by one of Q⊢P→Q.
  • (b) Suppose ⊥E were dropped. Derive ¬P⊢P→⊥ without it, and say what this derivation stops short of.
  • (c) Suppose instead →I were allowed only when the box’s assumption is cited by some line of the box or is itself the box’s last line. Which of the two derivations of (a) is lost? Is the one-line box of ⊢P→P lost? Is the sequent Q⊢P→Q lost?
  • (d) Let n be an integer. For n=3, n=6 and n=8, write the instance of “if n is a multiple of 4, then n is even”, and say for each whether the first sequent of (a), the second, or neither, decides its truth.

Solution.

  • (a) ¬P⊢P→Q: →I, ¬E, ⊥E (Proposition 2.1.2). Q⊢P→Q: →I and repetition.

  • (b) Four lines:

    1¬P
    2Pasm, for →I
    3⊥¬E 2, 1
    4P→⊥→I 2–3

    It stops at ⊥ inside the box, where the derivation of Proposition 2.1.2 wrote Q: the step from ⊥ to Q was ⊥E’s. What survives says only that P leads to a contradiction.

  • (c) The derivation of Q⊢P→Q is lost: no line of its box cites the assumption P (line 3 repeats line 1). The box of ⊢P→P is kept: its last line is its assumption, which the restriction allows. The derivation of Proposition 2.1.2 is kept: line 3 cites the assumption. But the sequent Q⊢P→Q is not lost. This derivation meets the restriction, since line 3 cites the assumption:
    1Q
    2Pasm, for →I
    3P∧Q∧I 2, 1
    4Q∧E 3
    5P→Q→I 2–4

    The restriction kills one derivation, not the sequent; a logic that really rejects the paradox has to restrict more than one rule.

  • (d) n=3: “if 3 is a multiple of 4, then 3 is even”; hypothesis and conclusion are both false, so only ¬P⊢P→Q decides it. n=6: “if 6 is a multiple of 4, then 6 is even”; the hypothesis is false and the conclusion true, so either sequent decides it. n=8: “if 8 is a multiple of 4, then 8 is even”; both parts are true (8=4⋅2), so the first sequent does not apply and the second does, since the conclusion is true. This is the one instance of the three whose hypothesis holds, the kind in which the theorem says something: here it can be fired by →E.

Marking scheme. (10 points) 2: (a), both rule lists. 2: (b), a correct four-line derivation (1) and the remark that the step to Q is ⊥E’s (1). 3: (c), the right derivation lost and the reason, that the assumption is never cited (1); ⊢P→P kept (1); and a derivation of Q⊢P→Q that meets the restriction (1). 3: (d), one point per value: the truth values of hypothesis and conclusion, and the right sequent (n=3: the first only; n=6: either; n=8: the second). Fatal error (0 for (b)): a derivation of P→Q itself without ⊥E that cites a line inside a closed box.

C. Going deeper

Exercise (C1: A disjunct that cannot hold)
  • (a) Show that P∨(Q∧¬Q)⊢P.
  • (b) What does (a) say about the statement “x>0, or x=1 and x≠1”, for a real number x?

Solution.

  • (a) The premise is a disjunction, so split it by ∨E, with both boxes ending in the goal P. The box of P is a one-line box. The box of Q∧¬Q is impossible: ∧E gives a clash, and ⊥E closes the case.
    1P∨(Q∧¬Q)
    2Pasm, for ∨E
    3Q∧¬Qasm, for ∨E
    4Q∧E 3
    5¬Q∧E 3
    6⊥¬E 4, 5
    7P⊥E 6
    8P∨E 1, 2–2, 3–7
  • (b) With P: “x>0” and Q: “x=1”, the statement is P∨(Q∧¬Q), since x≠1 is ¬(x=1). By (a), it gives x>0. So the second disjunct adds nothing: a disjunct that can never hold is an impossible case, and it closes itself. (Conversely, x>0 gives the whole statement by ∨I, so the two say the same thing.)
Exercise (C2: A clash that escaped its box)

A student wants to show ¬P⊢P→Q and writes:

1¬P
2P
3⊥¬E 2, 1
4Q⊥E 3
5Pasm, for →I
6QR 4
7P→Q→I 5–6
  • (a) Is the sequent ¬P⊢P→Q derivable?
  • (b) Find the first line that is not justified, and name the clause of Definition 1.4.2 it breaks.
  • (c) Show that the move made at that line can lead from a true premise to a false conclusion.
  • (d) Write a correct derivation.

Solution.

  • (a) Yes: it is Proposition 2.1.2. The conclusion is true; the question is whether this argument proves it.

  • (b) Line 4. It cites line 3, which lies inside the box 2–3, and that box has closed before line 4. By the scope rule of Definition 1.4.2, a line inside a closed box is not available. (Lines 1–3 are fine: a box may close without a rule discharging it, although nothing then leaves it. Lines 5–7 would be fine if line 4 were.)

  • (c) Lines 1–4 alone would “derive” ¬P⊢Q by the same move. Read P as “x>0” and Q as “x=7”, and take x=−1. The premise ¬(x>0) is true, and the conclusion x=7 is false. So the move “write, outside a box, what a closed box’s ⊥ would allow” can lead from a true premise to a false line. The line ⊥ on line 3 holds only under the assumption P; once the box closes, that assumption is gone, and so is the clash.

  • (d) Move the ⊥E inside the box, where the clash is:

1¬P
2Pasm, for →I
3⊥¬E 2, 1
4Q⊥E 3
5P→Q→I 2–4

Marking scheme. (10 points) - 2: answers (a) yes, citing Proposition 2.1.2 or giving a derivation. - 3: names line 4 as the first failure and the scope rule (a line inside a closed box is not available) as the clause broken. - 3: gives a counterexample to the step, not only to some conclusion: a reading of P, Q under which lines 1–4 go from a true premise to a false line. - 2: a correct derivation, with every citation available.

Fatal errors (0 for the step): blaming line 7 or line 6 (they are correct once line 4 is); saying that ⊥E itself is the error.