2.5 Proof by Contradiction and the Classical Rules

Every rule so far either builds a statement or takes one apart. The rules for negation are no exception: $\mathrm{\neg I}$ (Definition 2.2.1) builds $\neg\varphi$ from a box that opens with $\varphi$ and ends in $\bot$ , and $\mathrm{\neg E}$ (Definition 2.1.1) uses $\neg\varphi$ against $\varphi$ . Yet in three places this chapter has stopped one step short of a goal. This section adds the one rule that takes a negation away, reductio ad absurdum. It then derives from it the classical laws that mathematics uses without noticing, and shows that three of them are one principle in three forms.

2.5.1. Two boxes that look alike

Here are two arguments that a mathematician would both call “proof by contradiction”.

The first is the proof of Theorem 2.2.1. It fixes a rational number $r$ , supposes $r^2 = 2$ , reaches a contradiction, and concludes that $r^2 \ne 2$ . In the language of Definition 2.2.1, it opens a box with the assumption $P$ (“ $r^2 = 2$ ”), reaches $\bot$ inside it, and closes the box to get $\neg P$ . That is $\mathrm{\neg I}$ .

The second is about a real number.

Example (A number whose square is at most itself)

Let $x$ be a real number with $x^2 \le x$ . Prove that $x \le 1$ .

Solution. Suppose, for a contradiction, that $x \le 1$ fails, that is, $x > 1$ . Then $x > 0$ , and multiplying $x > 1$ by $x$ gives $x^2 > x$ . This contradicts $x^2 \le x$ . Hence $x \le 1$ .

Look at its shape. The box opens with the assumption $\neg P$ , where $P$ is “ $x \le 1$ ”, reaches $\bot$ , and closes to give $P$ . If we tried to justify the last line by $\mathrm{\neg I}$ , we would get the negation of the box’s assumption, $\neg\neg P$ : “it is not the case that $x \le 1$ fails”. That is not $P$ . The two arguments put their negations in different places. $\mathrm{\neg I}$ puts a $\neg$ into the conclusion; the second argument takes one out.

2.5.2. Where the rules so far stop short

The second argument is not a curiosity. Three times already in this chapter a derivation has stopped short in the same way: it reached a negation where the goal was not one.

Section 2.2 noted that a box opened with $\neg(x > 0)$ and closed by $\mathrm{\neg I}$ gives $\neg\neg(x > 0)$ , and no rule so far gets from there to $x > 0$ .
If you did Exercise C1 of Section 2.3, you met a second: Exercise (C1: Two premises that cannot both fail, used later) led from $P \to Q$ and $\neg P \to R$ to $\neg(\neg Q \wedge \neg R)$ , and not to $Q \vee R$ .
Section 2.4 noted, after Example (Negating both sides of an iff), that its converse, $\neg P \leftrightarrow \neg Q \vdash P \leftrightarrow Q$ , resists the rules so far. The natural box on $\neg Q$ , inside the box of $P$ , closes to $\neg\neg Q$ , not $Q$ .

Try the smallest case, $P$ from $\neg\neg P$ . The goal $P$ is a letter, so no introduction rule applies: the goal-directed moves have nothing to say. The premise $\neg\neg P$ is a negation, and a negation can be used only by $\mathrm{\neg E}$ , against the statement it negates, $\neg P$ . So we assume $\neg P$ in a box. The box reaches $\bot$ at once, and $\mathrm{\neg I}$ closes it with $\neg\neg P$ : the premise again. Every attempt goes round this circle.

That no derivation of $P$ from $\neg\neg P$ exists with the rules so far is a claim about all derivations, which no search can settle; this section’s Looking-ahead box says where it is proved. Here we name the missing step and add it as a rule.

2.5.3. Reductio ad absurdum

To prove $\varphi$ , it is enough to show that “not $\varphi$ ” leads to a contradiction.

Definition 2.5.1 (Reductio ad Absurdum)

i

\neg \varphi

asm, for

\mathrm{RAA}

\vdots

j

\bot

k

\varphi

\mathrm{RAA}

i

–

j

This is the rule $\mathrm{RAA}$ (reductio ad absurdum, “reduction to the absurd”). The line $\neg\varphi$ is an assumption, which opens the box and is discharged when the box closes. The line $\bot$ is a line of that box itself, not of a box inside it.

As in every schema (Definition 1.2.1), $\varphi$ stands for any statement and $i, j, k$ for line numbers. This rule has conditions that matter; read each one.

The assumption is the exact negation of the goal. To prove $\varphi$ , the box opens with $\neg\varphi$ : the negation of the whole of $\varphi$ . If $\varphi$ is $Q \vee R$ , the box opens with $\neg(Q \vee R)$ , not with $\neg Q \vee R$ . In a finished derivation this assumption is printed “asm, for $\mathrm{RAA}$ ”; in prose it is the sentence “suppose, for a contradiction, that $\varphi$ fails”.
The box must reach $\bot$ , as a line of the box itself: a $\bot$ inside a smaller box depends on a further assumption, as in $\mathrm{\neg I}$ .
The result is $\varphi$ itself, not $\neg\neg\varphi$ , which $\mathrm{\neg I}$ would give from the same box. This clause is the whole content of the rule.
The box closes, its assumption is discharged, and the justification cites the box as a range $i\text{–}j$ .

In words: the box is a thought experiment in which $\varphi$ fails. If the experiment ends in $\bot$ , then $\varphi$ cannot fail, and $\mathrm{RAA}$ lets us write $\varphi$ . Set the new rule beside $\mathrm{\neg I}$ :

Rule	The box opens with	The box ends with	After the box
$\mathrm{\neg I}$	$\varphi$	$\bot$	$\neg\varphi$
$\mathrm{RAA}$	$\neg\varphi$	$\bot$	$\varphi$

The rows differ only in where the $\neg$ sits, and that makes $\mathrm{RAA}$ different in kind: every other primitive rule is the introduction or elimination rule of one connective ( $\mathrm{\bot E}$ counts as the elimination rule of $\bot$ , and $\mathrm{R}$ is the repetition clause of Definition 1.4.2), while $\mathrm{RAA}$ applies to every statement, whatever its main connective, even a letter.

In the Givens/Goal table, $\mathrm{RAA}$ adds $\neg\varphi$ to the Givens and makes $\bot$ the goal.

With the convention of Section 2.1, the argument of Example (A number whose square is at most itself) is this derivation.

x^2 \le x

\neg (x \le 1)

asm, for

\mathrm{RAA}

x > 1

algebra 2

\neg (x^2 \le x)

algebra 3

\bot

\mathrm{{\neg}E}

1, 4

x \le 1

\mathrm{RAA}

2–5

Warning. The assumption that opens an $\mathrm{RAA}$ box must be the exact negation of the goal. To prove $x \le 1$ by contradiction, assume $x > 1$ , since for real numbers “not $x \le 1$ ” says $x > 1$ . Assuming $x \ge 1$ instead is a common slip. It is not the negation: $x = 1$ satisfies both $x \le 1$ and $x \ge 1$ . A box opened with $x \ge 1$ cannot honestly reach $\bot$ while $x = 1$ is possible, so a “contradiction” that seems to be reached hides an error.

Quick check. A box opens with the assumption $\neg(x < 0)$ and reaches $\bot$ , as a line of the box itself. Which of the following may be written after it closes, and by which rule? (i) $x < 0$ ; (ii) $\neg\neg(x < 0)$ ; (iii) $x \ge 0$ .

Solution.

(i) By $\mathrm{RAA}$ : the box opened with the negation of $x < 0$ . (ii) By $\mathrm{\neg I}$ : $\mathrm{\neg I}$ writes the negation of the box’s assumption, and the assumption is $\neg(x < 0)$ . (iii) By neither. For real numbers $x \ge 0$ says the same as $\neg(x < 0)$ , which is exactly the statement the box has refuted.

Quick check. In the derivation of Example (A number whose square is at most itself) above, which line is the $\mathrm{RAA}$ step, which box does it cite, and what would $\mathrm{\neg I}$ have written there instead?

Solution. Line 6 is the $\mathrm{RAA}$ step, and it cites the box $2\text{–}5$ . $\mathrm{\neg I}$ would have written $\neg\neg(x \le 1)$ .

2.5.4. The move: when stuck, assume the negation of the goal

Chapter 1 and Sections 2.1–2.4 built two lists of moves. From the goal: its main connective chooses an introduction rule and so a box or two subgoals. From the premises: each available line’s main connective chooses the elimination rule that uses it, and a goal $\bot$ asks for a clash. The new rule adds one move, for the moment when both lists are used up.

We are stuck at a gap when the goal-directed moves give nothing (the goal is a letter, or a disjunction with neither side in hand) and no premise-directed move brings the goal closer. Then open an $\mathrm{RAA}$ box on the negation of the goal. The new goal is $\bot$ , so we hunt for a clash, and the box has given us one more line to clash with: $\neg\varphi$ itself.

When stuck, assume the negation of the goal, and hunt for a clash.

The move is a last resort, not a first one: try every other move first. Four of the derivations under the next heading reach the moment of being stuck, and their Ideas say where.

When $\mathrm{RAA}$ earns its place. Look ahead at where the classical step enters the derivations below: a goal that is a letter with nothing to build it (Proposition 2.5.1), and a disjunction neither of whose sides follows from what is available, each side’s step breaking on its own (Proposition 2.5.3, De Morgan’s law (d)). Premises that say little and a goal that decides something: that is where to expect $\mathrm{RAA}$ . Exercise B6 meets a third such disjunction.

2.5.5. Derivations with the new rule

The stall, resolved. The next result is the one on which we got stuck.

Proposition 2.5.1 (Double Negation)

For every statement $P$ :

(a) $P \vdash \neg\neg P$ , by a derivation that does not use $\mathrm{RAA}$ ;
(b) $\neg\neg P \vdash P$ , by a derivation that uses $\mathrm{RAA}$ .

Idea. In (a) the goal $\neg\neg P$ is the negation of $\neg P$ , so the goal-directed move of Section 2.2 opens a $\mathrm{\neg I}$ box with $\neg P$ , and the premise clashes with it at once.

In (b) the goal $P$ is a letter, so no introduction rule applies. The only premise is a negation, which can only clash; the attempt above showed that clashing it inside a $\mathrm{\neg I}$ box leads back to the premise. We are stuck, so we assume the negation of the goal: an $\mathrm{RAA}$ box on $\neg P$ . The premise clashes with it at once.

Proof.

(a) This is the derivation of Example (Two negations from one premise) (a), which uses the rules of Definition 2.2.1 alone; we repeat it to set it beside (b).
1 $P$
2 $\neg P$ asm, for $\mathrm{{\neg}I}$
3 $\bot$ $\mathrm{{\neg}E}$ 1, 2
4 $\neg\neg P$ $\mathrm{{\neg}I}$ 2–3
(b) An $\mathrm{RAA}$ box on $\neg P$ :

\neg\neg P

\neg P

asm, for

\mathrm{RAA}

\bot

\mathrm{{\neg}E}

2, 1

P

\mathrm{RAA}

2–3

Line 3 applies $\mathrm{\neg E}$ to the statement $\neg P$ on line 2 and to its negation $\neg\neg P$ on line 1. This proves both parts.

In both derivations, lines 2 and 3 form a box that opens with $\neg P$ and reaches $\bot$ by a clash with line 1. Only the rule that closes the box differs, and with it the last line. So the two directions are not mirror images: one needs only the rules for $\neg$ , and the derivation of the other uses the new rule.

Second readingEdge cases of reductio

The degenerate case. The smallest use of $\mathrm{RAA}$ proves $P$ from $P$ .

Idea. There is nothing to find: the premise is the goal. The derivation is here only to show the rule at its smallest. The box opens with $\neg P$ , and the one line it needs, $\bot$ , comes from the clash of the assumption with the premise.

P

\neg P

asm, for

\mathrm{RAA}

\bot

\mathrm{{\neg}E}

1, 2

P

\mathrm{RAA}

2–3

It is legal and pointless, since line 1 already is the goal. It is the purest case of a pattern that turns up in real proofs: a contradiction box whose assumption does nothing except clash with a line we already had. A warning later in this section, after Example (A number below every positive number), returns to it.

Nonexample by minimal change. Change only the last line of (a), from $\neg\neg P$ to $P$ , keeping the justification $\mathrm{\neg I}\ 2\text{–}3$ . Lines 1–3 still check. What fails is the conclusion of $\mathrm{\neg I}$ , which must be the negation of the box’s assumption, here $\neg\neg P$ . To write $P$ , the justification must be $\mathrm{RAA}$ .

From now on both parts are derived rules in the sense of Definition 2.3.1. A line $\neg\neg\varphi$ may be justified by “ $\mathrm{\neg\neg I}$ $i$ ”, citing a line $\varphi$ , and a line $\varphi$ by “ $\mathrm{\neg\neg E}$ $i$ ”, citing a line $\neg\neg\varphi$ . The first stall of the list above is now one line: from $\neg\neg(x > 0)$ , $\mathrm{\neg\neg E}$ gives $x > 0$ .

Contraposition, backwards. Proposition 2.3.2 derives $\neg Q \to \neg P$ from $P \to Q$ with the rules for $\to$ and $\neg$ alone. In practice we use it the other way round. To prove “if $n^2$ is even then $n$ is even”, one may prove “if $n$ is not even then $n^2$ is not even”, and the step from that back to the original goes from $\neg Q \to \neg P$ to $P \to Q$ .

Proposition 2.5.2 (Converse of the Contrapositive)

For all statements $P$ and $Q$ , $\neg Q \to \neg P \vdash P \to Q$ .

Idea. The goal is an implication, so the goal-directed move opens a box with $P$ , and the new goal is $Q$ , a letter. The premise needs $\neg Q$ before it gives anything, and $\neg Q$ is nowhere; the box’s assumption $P$ is a letter and cannot be taken apart. We are stuck at $Q$ , so we assume its negation, $\neg Q$ . That is exactly what the premise wanted: $\mathrm{{\to}E}$ gives $\neg P$ , which clashes with the $P$ of the outer box, and $\mathrm{RAA}$ closes the inner box with $Q$ .

In pictures: the stall at the letter $Q$ ; then the $\mathrm{RAA}$ box on $\neg Q$ .

\neg Q \to \neg P

P

asm, for

\mathrm{{{\to}}I}

\vdots

Q

P \to Q

\mathrm{{{\to}}I}

2–6

\neg Q \to \neg P

P

asm, for

\mathrm{{{\to}}I}

\neg Q

asm, for

\mathrm{RAA}

\vdots

\bot

Q

\mathrm{RAA}

3–5

P \to Q

\mathrm{{{\to}}I}

2–6

Proof. The derivation is:

\neg Q \to \neg P

P

asm, for

\mathrm{{{\to}}I}

\neg Q

asm, for

\mathrm{RAA}

\neg P

\mathrm{{{\to}}E}

1, 3

\bot

\mathrm{{\neg}E}

2, 4

Q

\mathrm{RAA}

3–5

P \to Q

\mathrm{{{\to}}I}

2–6

Line 5 may cite line 2 because line 2 lies in a box that is still open. $\mathrm{RAA}$ enters at line 6. This proves the proposition.

So contraposition behaves like double negation: going from $P \to Q$ to $\neg Q \to \neg P$ needs no $\mathrm{RAA}$ , and our derivation of the way back uses one $\mathrm{RAA}$ .

Excluded middle. Every integer is even or odd. Every real number is $\ge 0$ or $< 0$ . The purely logical form of such facts is the law $P \vee \neg P$ , which the next result derives from no premises at all.

Proposition 2.5.3 (Excluded Middle)

For every statement $P$ , $\vdash P \vee \neg P$ .

Idea. The goal is a disjunction, so Section 1.5’s move postpones it: choose a side only when that side is in hand. But there are no premises, so no premise-directed move applies, and neither side is worth aiming at: $P$ false breaks the step to $P$ , and $P$ true breaks the step to $\neg P$ . We are stuck, so we assume the negation of the whole goal, $\neg(P \vee \neg P)$ , which says that neither side holds, and hunt for a clash. The new line can clash only with $P \vee \neg P$ , which $\mathrm{\vee I}$ builds from either side. So we manufacture a side, as in Example (Manufacturing the other half of a clash). If $P$ held, then $P \vee \neg P$ would hold, against the assumption; so $\neg P$ , by $\mathrm{\neg I}$ . But then $P \vee \neg P$ holds after all, and that is the final clash.

In pictures: the $\mathrm{RAA}$ box; then the final clash, written backwards.

\neg (P \vee \neg P)

asm, for

\mathrm{RAA}

\vdots

\bot

P \vee \neg P

\mathrm{RAA}

1–7

\neg (P \vee \neg P)

asm, for

\mathrm{RAA}

\vdots

\neg P

P \vee \neg P

\mathrm{{\vee}I}

\bot

\mathrm{{\neg}E}

6, 1

P \vee \neg P

\mathrm{RAA}

1–7

Proof. The derivation is:

\neg (P \vee \neg P)

asm, for

\mathrm{RAA}

P

asm, for

\mathrm{{\neg}I}

P \vee \neg P

\mathrm{{\vee}I}

\bot

\mathrm{{\neg}E}

3, 1

\neg P

\mathrm{{\neg}I}

2–4

P \vee \neg P

\mathrm{{\vee}I}

\bot

\mathrm{{\neg}E}

6, 1

P \vee \neg P

\mathrm{RAA}

1–7

The derivation has no premises, so it shows $\vdash P \vee \neg P$ . $\mathrm{RAA}$ is used once, at line 8. This proves the proposition.

The assumption of line 1 is used twice, at lines 4 and 7. The first use refutes $P$ ; the second uses that refutation. Excluded middle now becomes a derived rule with no premises: a line $\varphi \vee \neg\varphi$ may be written anywhere, for any statement $\varphi$ , justified by $\mathrm{LEM}$ with no line cited. Pasting in the eight lines above would replace it.

Its use is proof by cases on a statement. To derive $\chi$ , derive it once in a box that assumes $\varphi$ and once in a box that assumes $\neg\varphi$ , and combine the two boxes with the line $\varphi \vee \neg\varphi$ by $\mathrm{\vee E}$ . The fold after De Morgan’s laws below uses it that way, and so does part (b) of the result after them.

A law with no negation. The last is a law in which $\neg$ does not occur at all.

Proposition 2.5.4 (Peirce’s Law)

For all statements $P$ and $Q$ , $\vdash ((P \to Q) \to P) \to P$ .

In words: a law with no $\neg$ in it, whose derivation here still uses $\mathrm{RAA}$ . The derivation is in the fold below.

Second readingPeirce’s law, derived

Try it first (ten minutes): use the goal-directed and premise-directed moves of the earlier sections on this goal until they stall. At which gap do they stall, and which line, if it were available there, would let you finish?

Idea. The goal is an implication, so we open a box on $(P \to Q) \to P$ with the goal $P$ , a letter. The only line that can produce $P$ is the assumption itself, by $\mathrm{{\to}E}$ , once we have its hypothesis $P \to Q$ . So $P \to Q$ becomes a subgoal, and the goal-directed move opens a box on $P$ with the goal $Q$ . There the moves stall: the resources are $(P \to Q) \to P$ and $P$ , and neither says anything about $Q$ . What the stalled gap lacks is a clash, which $\mathrm{\bot E}$ would turn into $Q$ .

We are stuck, so the new move applies, but where? Assuming $\neg Q$ at the stalled gap gives nothing new: a clash with $\neg Q$ needs $Q$ , the stalled goal itself. So apply the move one level out, to the goal $P$ , and assume $\neg P$ . That is exactly what the stalled gap lacked: inside the box of $P$ , the pair $P$ , $\neg P$ gives $\bot$ , and $\mathrm{\bot E}$ gives $Q$ . Then $P \to Q$ , then $P$ by $\mathrm{{\to}E}$ , which clashes with $\neg P$ .

Proof. The derivation is:

(P \to Q) \to P

asm, for

\mathrm{{{\to}}I}

\neg P

asm, for

\mathrm{RAA}

P

asm, for

\mathrm{{{\to}}I}

\bot

\mathrm{{\neg}E}

3, 2

Q

\mathrm{{\bot}E}

P \to Q

\mathrm{{{\to}}I}

3–5

P

\mathrm{{{\to}}E}

1, 6

\bot

\mathrm{{\neg}E}

7, 2

P

\mathrm{RAA}

2–8

((P \to Q) \to P) \to P

\mathrm{{{\to}}I}

1–9

The derivation has no premises, and $\mathrm{RAA}$ enters at line 9. This proves the proposition.

The assumption $\neg P$ of line 2 is used twice: at line 4 it makes the innermost box contradictory, and at line 8 it clashes with the $P$ that line 7 obtained. Notice where the new box went: around the stalled box, not inside it. An assumption made one level out is available in every gap inside its box, and so it could give the stalled gap the line it lacked. Peirce’s law contains no $\neg$ , yet our derivation uses $\mathrm{RAA}$ : the classical rule is about more than negation.

2.5.6. De Morgan’s laws

The negation of an “and” is an “or” of negations, and the negation of an “or” is an “and” of negations. For example, a real number $x$ fails to lie in the interval $[0, 1]$ , that is, $\neg(0 \le x \wedge x \le 1)$ , exactly when $x < 0$ or $x > 1$ . Each law has two directions, so there are four derivations to give.

Proposition 2.5.5 (De Morgan’s Laws)

For all statements $P$ and $Q$ :

(a) $\neg(P \vee Q) \vdash \neg P \wedge \neg Q$ ;
(b) $\neg P \wedge \neg Q \vdash \neg(P \vee Q)$ ;
(c) $\neg P \vee \neg Q \vdash \neg(P \wedge Q)$ ;
(d) $\neg(P \wedge Q) \vdash \neg P \vee \neg Q$ .

Try it first (ten minutes): look for a derivation of (d) with the rules of the earlier sections. Which rule would give its last line, and what would that rule need?

Idea. Parts (a)–(c) yield to their goals. In (a) the goal is a conjunction of negations: two $\mathrm{\neg I}$ boxes, one per conjunct. In (b) and (c) the goal is a negation: one $\mathrm{\neg I}$ box, with the disjunction used inside it by $\mathrm{\vee E}$ .

In pictures, for (a): two subgoals; then a box under each.

\neg (P \vee Q)

\vdots

\neg P

\vdots

\neg Q

\neg P \wedge \neg Q

\mathrm{{\wedge}I}

5, 9

\neg (P \vee Q)

P

asm, for

\mathrm{{\neg}I}

\vdots

\bot

\neg P

\mathrm{{\neg}I}

2–4

Q

asm, for

\mathrm{{\neg}I}

\vdots

\bot

\neg Q

\mathrm{{\neg}I}

6–8

\neg P \wedge \neg Q

\mathrm{{\wedge}I}

5, 9

For (b): the box on $P \vee Q$ ; then the two cases inside it.

\neg P \wedge \neg Q

\neg P

\mathrm{{\wedge}E}

\neg Q

\mathrm{{\wedge}E}

P \vee Q

asm, for

\mathrm{{\neg}I}

\vdots

\bot

\neg (P \vee Q)

\mathrm{{\neg}I}

4–9

\neg P \wedge \neg Q

\neg P

\mathrm{{\wedge}E}

\neg Q

\mathrm{{\wedge}E}

P \vee Q

asm, for

\mathrm{{\neg}I}

P

asm, for

\mathrm{{\vee}E}

\vdots

\bot

Q

asm, for

\mathrm{{\vee}E}

\vdots

\bot

\bot

\mathrm{{\vee}E}

4, 5–6, 7–8

\neg (P \vee Q)

\mathrm{{\neg}I}

4–9

Part (d) resists. Its goal is a disjunction, so the natural last line is $\mathrm{\vee I}$ , from $\neg P$ or from $\neg Q$ . But the step from the premise to $\neg P$ can be broken: with $P$ true and $Q$ false the premise is true and $\neg P$ false; and the step to $\neg Q$ breaks with $P$ false and $Q$ true. So neither side is worth aiming at. The premise itself can be used only by $\mathrm{\neg E}$ , against $P \wedge Q$ , which we do not have. We are stuck at the whole goal, so we assume its negation, $\neg(\neg P \vee \neg Q)$ , which says that neither $\neg P$ nor $\neg Q$ holds. It should give $P$ and $Q$ . Each is a letter, so each gets a small $\mathrm{RAA}$ box of its own, whose clash is manufactured by $\mathrm{\vee I}$ . Together $P$ and $Q$ clash with the premise.

For (d): the $\mathrm{RAA}$ box on the negated goal; then a box for each of $P$ and $Q$ .

\neg (P \wedge Q)

\neg (\neg P \vee \neg Q)

asm, for

\mathrm{RAA}

\vdots

P \wedge Q

\bot

\mathrm{{\neg}E}

11, 1

\neg P \vee \neg Q

\mathrm{RAA}

2–12

\neg (P \wedge Q)

\neg (\neg P \vee \neg Q)

asm, for

\mathrm{RAA}

\neg P

asm, for

\mathrm{RAA}

\vdots

\bot

P

\neg Q

asm, for

\mathrm{RAA}

\vdots

\bot

Q

P \wedge Q

\mathrm{{\wedge}I}

6, 10

\bot

\mathrm{{\neg}E}

11, 1

\neg P \vee \neg Q

\mathrm{RAA}

2–12

Proof.

(a) Two $\mathrm{\neg I}$ boxes, one for each conjunct, then $\mathrm{\wedge I}$ :
1 $\neg (P \vee Q)$
2 $P$ asm, for $\mathrm{{\neg}I}$
3 $P \vee Q$ $\mathrm{{\vee}I}$ 2
4 $\bot$ $\mathrm{{\neg}E}$ 3, 1
5 $\neg P$ $\mathrm{{\neg}I}$ 2–4
6 $Q$ asm, for $\mathrm{{\neg}I}$
7 $P \vee Q$ $\mathrm{{\vee}I}$ 6
8 $\bot$ $\mathrm{{\neg}E}$ 7, 1
9 $\neg Q$ $\mathrm{{\neg}I}$ 6–8
10 $\neg P \wedge \neg Q$ $\mathrm{{\wedge}I}$ 5, 9
(b) One $\mathrm{\neg I}$ box that opens with $P \vee Q$ . Inside it, $\mathrm{\vee E}$ splits into two cases, and each case clashes with one half of the premise:
1 $\neg P \wedge \neg Q$
2 $\neg P$ $\mathrm{{\wedge}E}$ 1
3 $\neg Q$ $\mathrm{{\wedge}E}$ 1
4 $P \vee Q$ asm, for $\mathrm{{\neg}I}$
5 $P$ asm, for $\mathrm{{\vee}E}$
6 $\bot$ $\mathrm{{\neg}E}$ 5, 2
7 $Q$ asm, for $\mathrm{{\vee}E}$
8 $\bot$ $\mathrm{{\neg}E}$ 7, 3
9 $\bot$ $\mathrm{{\vee}E}$ 4, 5–6, 7–8
10 $\neg (P \vee Q)$ $\mathrm{{\neg}I}$ 4–9
(c) The same shape as (b), with the roles of $\wedge$ and $\vee$ exchanged:
1 $\neg P \vee \neg Q$
2 $P \wedge Q$ asm, for $\mathrm{{\neg}I}$
3 $P$ $\mathrm{{\wedge}E}$ 2
4 $Q$ $\mathrm{{\wedge}E}$ 2
5 $\neg P$ asm, for $\mathrm{{\vee}E}$
6 $\bot$ $\mathrm{{\neg}E}$ 3, 5
7 $\neg Q$ asm, for $\mathrm{{\vee}E}$
8 $\bot$ $\mathrm{{\neg}E}$ 4, 7
9 $\bot$ $\mathrm{{\vee}E}$ 1, 5–6, 7–8
10 $\neg (P \wedge Q)$ $\mathrm{{\neg}I}$ 2–9
(d) $\mathrm{RAA}$ on the goal, and inside it two smaller $\mathrm{RAA}$ boxes:

\neg (P \wedge Q)

\neg (\neg P \vee \neg Q)

asm, for

\mathrm{RAA}

\neg P

asm, for

\mathrm{RAA}

\neg P \vee \neg Q

\mathrm{{\vee}I}

\bot

\mathrm{{\neg}E}

4, 2

P

\mathrm{RAA}

3–5

\neg Q

asm, for

\mathrm{RAA}

\neg P \vee \neg Q

\mathrm{{\vee}I}

\bot

\mathrm{{\neg}E}

8, 2

Q

\mathrm{RAA}

7–9

P \wedge Q

\mathrm{{\wedge}I}

6, 10

\bot

\mathrm{{\neg}E}

11, 1

\neg P \vee \neg Q

\mathrm{RAA}

2–12

The derivations of (a), (b), and (c) close every box by $\mathrm{\neg I}$ or $\mathrm{\vee E}$ and use no $\mathrm{RAA}$ . The derivation of (d) uses $\mathrm{RAA}$ at lines 6, 10, and 13. This proves all four laws.

Laws (a)–(c) conclude negations or a conjunction of negations, and $\mathrm{\neg I}$ builds negations. Law (d) concludes a disjunction, and $\mathrm{\vee I}$ needs to know which side holds, while the premise says only that $P$ and $Q$ do not both hold. $\mathrm{RAA}$ gets round the missing decision without making it.

Second readingDe Morgan (d) by excluded middle

Excluded middle makes the decision instead. Split on $P \vee \neg P$ . In the case $\neg P$ , $\mathrm{\vee I}$ gives $\neg P \vee \neg Q$ at once. In the case $P$ , a $\mathrm{\neg I}$ box on $Q$ builds $P \wedge Q$ , which clashes with the premise, giving $\neg Q$ ; then $\mathrm{\vee I}$ gives $\neg P \vee \neg Q$ . Written out, this route is 11 lines, with $\mathrm{LEM}$ as its one classical line. Both routes use a classical rule.

Quick check. Suppose $\mathrm{RAA}$ were deleted from the list of rules. Which of the four derivations in the proof of Proposition 2.5.5 would still be correct, and what is the first line of the others that would lose its justification?

Solution. The derivations of (a), (b), and (c) would still be correct: they use $\mathrm{\neg I}$ , $\mathrm{\neg E}$ , $\mathrm{\vee I}$ , $\mathrm{\vee E}$ , $\mathrm{\wedge I}$ , and $\mathrm{\wedge E}$ only. In the derivation of (d), line 6 is the first to lose its justification: it closes the box that opened with $\neg P$ and writes $P$ , which is $\mathrm{RAA}$ . (Lines 10 and 13 lose theirs too.)

2.5.7. Implication as a disjunction

In everyday mathematics “if $P$ then $Q$ ” and “either $P$ fails or $Q$ holds” are used interchangeably. One direction of that exchange needs only the earlier rules; our derivation of the other uses a classical rule.

Proposition 2.5.6 (Implication as a Disjunction)

For all statements $P$ and $Q$ :

(a) $\neg P \vee Q \vdash P \to Q$ , by a derivation that does not use $\mathrm{RAA}$ ;
(b) $P \to Q \vdash \neg P \vee Q$ , by a derivation that uses $\mathrm{LEM}$ .

Idea.

(a) The premise is a disjunction, so we use it by cases, each ending in the current goal $P \to Q$ . In each case that goal is an implication, so we open a box with $P$ . In the case $\neg P$ , the box clashes at once and $\mathrm{\bot E}$ gives $Q$ : this is the derivation of Proposition 2.1.2. In the case $Q$ , the box repeats $Q$ .
In pictures, for (a): the two cases; then a box on $P$ in each.

1 $\neg P \vee Q$
2 $\neg P$ asm, for $\mathrm{{\vee}E}$
$\vdots$
6 $P \to Q$
7 $Q$ asm, for $\mathrm{{\vee}E}$
$\vdots$
10 $P \to Q$
11 $P \to Q$ $\mathrm{{\vee}E}$ 1, 2–6, 7–10
1 $\neg P \vee Q$
2 $\neg P$ asm, for $\mathrm{{\vee}E}$
3 $P$ asm, for $\mathrm{{{\to}}I}$
$\vdots$
5 $Q$
6 $P \to Q$ $\mathrm{{{\to}}I}$ 3–5
7 $Q$ asm, for $\mathrm{{\vee}E}$
8 $P$ asm, for $\mathrm{{{\to}}I}$
$\vdots$
9 $Q$
10 $P \to Q$ $\mathrm{{{\to}}I}$ 8–9
11 $P \to Q$ $\mathrm{{\vee}E}$ 1, 2–6, 7–10
(b) The goal is a disjunction, so we postpone it. The premise is an implication, which gives $Q$ only once we have $P$ , and we do not. So we are stuck, and this time excluded middle is the better tool than an $\mathrm{RAA}$ box: we decide $P$ first. In the case $P$ the premise gives $Q$ ; in the case $\neg P$ the left side is in hand.

For (b): the split; then $\mathrm{{\to}E}$ in the case $P$ .

P \to Q

P \vee \neg P

\mathrm{LEM}

P

asm, for

\mathrm{{\vee}E}

\vdots

\neg P \vee Q

\neg P

asm, for

\mathrm{{\vee}E}

\vdots

\neg P \vee Q

\neg P \vee Q

\mathrm{{\vee}E}

2, 3–5, 6–7

P \to Q

P \vee \neg P

\mathrm{LEM}

P

asm, for

\mathrm{{\vee}E}

Q

\mathrm{{{\to}}E}

1, 3

\vdots

\neg P \vee Q

\neg P

asm, for

\mathrm{{\vee}E}

\vdots

\neg P \vee Q

\neg P \vee Q

\mathrm{{\vee}E}

2, 3–5, 6–7

Proof.

(a) $\mathrm{\vee E}$ on the premise, with an implication built in each case:
1 $\neg P \vee Q$
2 $\neg P$ asm, for $\mathrm{{\vee}E}$
3 $P$ asm, for $\mathrm{{{\to}}I}$
4 $\bot$ $\mathrm{{\neg}E}$ 3, 2
5 $Q$ $\mathrm{{\bot}E}$ 4
6 $P \to Q$ $\mathrm{{{\to}}I}$ 3–5
7 $Q$ asm, for $\mathrm{{\vee}E}$
8 $P$ asm, for $\mathrm{{{\to}}I}$
9 $Q$ $\mathrm{R}$ 7
10 $P \to Q$ $\mathrm{{{\to}}I}$ 8–9
11 $P \to Q$ $\mathrm{{\vee}E}$ 1, 2–6, 7–10

Line 9 repeats line 7 inside the box of line 8, because $\mathrm{{\to}I}$ needs $Q$ as a line of that box itself.
(b) Cases on $P$ :

P \to Q

P \vee \neg P

\mathrm{LEM}

P

asm, for

\mathrm{{\vee}E}

Q

\mathrm{{{\to}}E}

1, 3

\neg P \vee Q

\mathrm{{\vee}I}

\neg P

asm, for

\mathrm{{\vee}E}

\neg P \vee Q

\mathrm{{\vee}I}

\neg P \vee Q

\mathrm{{\vee}E}

2, 3–5, 6–7

Line 2 is Proposition 2.5.3 used as a derived rule, and the only $\mathrm{RAA}$ is inside it. This proves both parts.

The two routes of the section now stand side by side. $\mathrm{RAA}$ assumes the goal fails and hunts for a clash; $\mathrm{LEM}$ splits on a statement of our choosing and gives each case a resource it lacked. When a premise is waiting for a statement $S$ (here $P \to Q$ waits for $P$ ), splitting on $S$ is usually the shorter route.

2.5.8. One principle in three forms

$\mathrm{RAA}$ gave us $\mathrm{\neg\neg E}$ and excluded middle. Had we added one of those two as the new primitive rule instead of $\mathrm{RAA}$ , would we have proved less?

To say this exactly, we need two rule forms and one notion. $\mathrm{\neg\neg E}$ taken as a rule says: if $\neg\neg\varphi$ stands on an available line, we may write $\varphi$ . $\mathrm{LEM}$ taken as a rule says: we may write $\varphi \vee \neg\varphi$ on any line, for any statement $\varphi$ , citing nothing. Given a list of rules, a rule $\mathsf{X}$ derives a rule $\mathsf{Y}$ over that list if every use of $\mathsf{Y}$ in a derivation can be replaced by a fragment that uses only $\mathsf{X}$ and the rules of the list, without changing the premises or the last line. Then every sequent derivable with $\mathsf{Y}$ added to the list is derivable with $\mathsf{X}$ added instead.

Theorem 2.5.7 (The Classical Rules Are Interderivable)

Over the primitive rules other than $\mathrm{RAA}$ , each of the three rules $\mathrm{RAA}$ , $\mathrm{\neg\neg E}$ , and $\mathrm{LEM}$ derives the other two. In particular, adding any one of the three to the other primitive rules gives the same derivable sequents.

In words: $\mathrm{RAA}$ , $\mathrm{\neg\neg E}$ and $\mathrm{LEM}$ are one principle in three forms; adding any one of them to the other rules proves exactly what adding any other does.

In the picture, an arrow from X to Y means that X derives Y over the other primitive rules; going round the solid cycle, each rule derives the other two. ① is Proposition 2.5.3 on the solid arrow and Proposition 2.5.1 (b) on the dashed one; ② closes the box by $\mathrm{\neg I}$ , then applies $\mathrm{\neg\neg E}$ ; ③ splits on $\varphi \vee \neg\varphi$ .

Diagram. Labels: textcircled scriptsize 1, textcircled scriptsize 3, textcircled scriptsize 2, neg negE

Part ② says that a step of $\mathrm{RAA}$ can be replaced by $\mathrm{\neg I}$ followed by $\mathrm{\neg\neg E}$ , keeping the box. On the derivation of Example (A number whose square is at most itself), line 6 becomes two lines:

x^2 \le x

\neg (x \le 1)

asm, for

\mathrm{{\neg}I}

x > 1

algebra 2

\neg (x^2 \le x)

algebra 3

\bot

\mathrm{{\neg}E}

1, 4

\neg\neg (x \le 1)

\mathrm{{\neg}I}

2–5

x \le 1

\mathrm{{\neg\neg}E}

Line 6 is correct by $\mathrm{\neg I}$ : the box opens with $\neg(x \le 1)$ , and $\neg\neg(x \le 1)$ is the negation of that assumption. The box itself is unchanged: both rules ask for $\bot$ as a line of the box, and differ only in what they write after it. Part ③, shown on the same example in the fold below, replaces that $\mathrm{\neg\neg E}$ line by a split written by $\mathrm{LEM}$ .

So the classical part of our rules is one extra principle, whichever of its three forms we write down.

Second readingPart ③ on the example, and the proof: replacing one rule by another

Part ③ on the example. Part ③ replaces the $\mathrm{\neg\neg E}$ line of ② by a split on $(x \le 1) \vee \neg(x \le 1)$ , written by $\mathrm{LEM}$ :

x^2 \le x

\neg (x \le 1)

asm, for

\mathrm{{\neg}I}

x > 1

algebra 2

\neg (x^2 \le x)

algebra 3

\bot

\mathrm{{\neg}E}

1, 4

\neg\neg (x \le 1)

\mathrm{{\neg}I}

2–5

(x \le 1) \vee \neg (x \le 1)

\mathrm{LEM}

x \le 1

asm, for

\mathrm{{\vee}E}

\neg (x \le 1)

asm, for

\mathrm{{\vee}E}

\bot

\mathrm{{\neg}E}

9, 6

x \le 1

\mathrm{{\bot}E}

x \le 1

\mathrm{{\vee}E}

7, 8–8, 9–11

The first case is the goal; the second clashes with line 6 and closes itself. Together, ② and ③ turned the one $\mathrm{RAA}$ line into steps of $\mathrm{\neg I}$ , $\mathrm{LEM}$ and the rules of the earlier sections: that is how $\mathrm{LEM}$ derives $\mathrm{RAA}$ .

Idea. Replacements can be chained, so it is enough to go once round a cycle. ① $\mathrm{RAA}$ derives the other two: that is Proposition 2.5.3 and Proposition 2.5.1 (b). ② $\mathrm{\neg\neg E}$ derives $\mathrm{RAA}$ : $\mathrm{\neg I}$ closes an $\mathrm{RAA}$ box, which runs from $\neg\varphi$ to $\bot$ , with $\neg\neg\varphi$ , and $\mathrm{\neg\neg E}$ finishes. ③ $\mathrm{LEM}$ derives $\mathrm{\neg\neg E}$ : split on $\varphi \vee \neg\varphi$ ; the case $\varphi$ is the goal, and the case $\neg\varphi$ clashes with $\neg\neg\varphi$ .

Before reading on: in the fragment for ③ below, which rule does line $k + 4$ use, and why may line $k + 3$ cite line $m$ ?

Proof. ① Suppose a derivation uses $\mathrm{\neg\neg E}$ at line $k$ , writing $\varphi$ and citing a line $m$ that holds $\neg\neg\varphi$ . Replace line $k$ by the last three lines of the derivation in Proposition 2.5.1 (b), with its premise replaced by line $m$ : a box opening with $\neg\varphi$ , the line $\bot$ by $\mathrm{\neg E}$ citing the assumption and line $m$ , and then $\varphi$ by $\mathrm{RAA}$ . A use of $\mathrm{LEM}$ , writing $\varphi \vee \neg\varphi$ , is replaced by the eight lines of the derivation in Proposition 2.5.3, with $\varphi$ for $P$ ; that derivation has no premises. So $\mathrm{RAA}$ derives $\mathrm{\neg\neg E}$ and $\mathrm{LEM}$ .

② Suppose a derivation uses $\mathrm{RAA}$ at line $k$ , closing a box, lines $i$ to $j$ , that opens with $\neg\varphi$ and ends with $\bot$ . Keep the box and replace line $k$ by two lines:

i

\neg \varphi

asm, for

\mathrm{{\neg}I}

\vdots

j

\bot

k

\neg\neg \varphi

\mathrm{{\neg}I}

i

–

j

k+1

\varphi

\mathrm{{\neg\neg}E}

k

Line $k$ is correct by $\mathrm{\neg I}$ , since the box opens with $\neg\varphi$ and $\neg\neg\varphi$ is the negation of that assumption. Both rules ask for $\bot$ as a line of the box itself, so the box needs no change. So $\mathrm{\neg\neg E}$ derives $\mathrm{RAA}$ .

③ Suppose a derivation uses $\mathrm{\neg\neg E}$ at line $k$ , writing $\varphi$ and citing a line $m$ that holds $\neg\neg\varphi$ . Replace line $k$ by six lines:

m

\neg\neg \varphi

\vdots

k

\varphi \vee \neg \varphi

\mathrm{LEM}

k+1

\varphi

asm, for

\mathrm{{\vee}E}

k+2

\neg \varphi

asm, for

\mathrm{{\vee}E}

k+3

\bot

\mathrm{{\neg}E}

k+2

m

k+4

\varphi

\mathrm{{\bot}E}

k+3

k+5

\varphi

\mathrm{{\vee}E}

k

k+1

–

k+1

k+2

–

k+4

The first case is a one-line box: it opens with $\varphi$ and so already ends with the goal. In the second case, line $k + 3$ may cite line $m$ , because line $m$ was available at the old line $k$ and every new line sits in the same boxes as the old line $k$ , or in boxes opened after it. No rule other than $\mathrm{LEM}$ and the rules of the list is used. So $\mathrm{LEM}$ derives $\mathrm{\neg\neg E}$ .

In each replacement the later lines are renumbered, and a later citation of the old line $k$ now cites the fragment’s last line, which holds the same statement in the same boxes. The premises and the last line of the derivation are unchanged.

Finally, replacements can be chained. $\mathrm{LEM}$ derives $\mathrm{RAA}$ : replace each use of $\mathrm{RAA}$ by the fragment of ②, and then each use of $\mathrm{\neg\neg E}$ so created by the fragment of ③. $\mathrm{\neg\neg E}$ derives $\mathrm{LEM}$ : replace each use of $\mathrm{LEM}$ by the derivation of ①, and then each use of $\mathrm{RAA}$ in it by the fragment of ②. With ①, ②, and ③, this shows that each of the three rules derives the other two, as claimed.

The base list matters: part ③ uses $\mathrm{\bot E}$ at line $k + 4$ , to close the impossible case as in Example (An impossible case).

Second readingOther books, and a rule we could drop

Remark. Some books call exactly our $\mathrm{RAA}$ “proof by contradiction” or PBC, and some take $\mathrm{\neg\neg E}$ as their primitive rule and derive $\mathrm{RAA}$ from it. By Theorem 2.5.7 nothing changes: all these choices prove the same sequents.

Remark. $\mathrm{\bot E}$ could have been dropped from the primitive rules, since $\mathrm{RAA}$ and repetition derive it (Exercise B3 below asks for the derivation). We keep it so that the primitive rules other than $\mathrm{RAA}$ form a system of their own.

2.5.9. How reductio looks in a mathematical proof

Here is an argument of a kind that analysis uses constantly; read it one sentence at a time, with the rule of each step in brackets.

Example (A number below every positive number)

Let $x$ be a real number with $x \ge 0$ , and suppose that $x \le \varepsilon$ for every real number $\varepsilon > 0$ . Prove that $x = 0$ .

Solution. Suppose, for a contradiction, that $x \ne 0$ . Since $x \ge 0$ and $x \ne 0$ , we have $x > 0$ . Then $\varepsilon \mathrel{:=} x/2$ is a real number with $\varepsilon > 0$ , so the hypothesis applies to it and gives $x \le x/2$ . Subtracting $x/2$ from both sides gives $x/2 \le 0$ , and multiplying by $2$ gives $x \le 0$ . This contradicts $x > 0$ . Hence $x = 0$ .

“Suppose, for a contradiction, that $x \ne 0$ .” [An $\mathrm{RAA}$ box opens, with $\neg(x = 0)$ , the exact negation of the goal $x = 0$ .]
“Since $x \ge 0$ and $x \ne 0$ , we have $x > 0$ .” Example (An impossible case)
“Then $\varepsilon \mathrel{:=} x/2$ is a real number with $\varepsilon > 0$ .” [School algebra.]
“So the hypothesis applies to it and gives $x \le x/2$ .” [The hypothesis is about every $\varepsilon > 0$ ; applying it to one is a step about “every”, used as ordinary reasoning (the note at the start of this chapter).]
“… gives $x/2 \le 0$ , and … $x \le 0$ .” [School algebra.]
“This contradicts $x > 0$ .” [ $\mathrm{\neg E}$ : for real numbers $x > 0$ is $\neg(x \le 0)$ , the negation of the line $x \le 0$ .]
“Hence $x = 0$ .” [ $\mathrm{RAA}$ closes the box.]

$\mathrm{\neg I}$ or $\mathrm{RAA}$ ? The phrase “suppose not” covers two rules. Here is one statement proved both ways, for a real number $x$ : if $x^3 < 0$ , then $x < 0$ .

By the contrapositive ( $\mathrm{CP}$ ). We prove that if $x \ge 0$ , then $x^3 \ge 0$ . Suppose $x \ge 0$ [assumption for $\mathrm{{\to}I}$ ]. Then $x^3 = x \cdot x \cdot x \ge 0$ [algebra]. So if $x \ge 0$ , then $x^3 \ge 0$ [ $\mathrm{{\to}I}$ ], and by contraposition, if $x^3$ is not $\ge 0$ , then $x$ is not $\ge 0$ [ $\mathrm{CP}$ ]: that is, if $x^3 < 0$ , then $x < 0$ .
By contradiction ( $\mathrm{RAA}$ ). Suppose $x^3 < 0$ [assumption for $\mathrm{{\to}I}$ ]. Suppose, for a contradiction, that $x < 0$ fails, that is, $x \ge 0$ [an $\mathrm{RAA}$ box on $\neg(x < 0)$ ]. Then $x^3 \ge 0$ , which contradicts $x^3 < 0$ [ $\mathrm{\neg E}$ ]. Hence $x < 0$ [ $\mathrm{RAA}$ ], and so if $x^3 < 0$ , then $x < 0$ [ $\mathrm{{\to}I}$ ].

The first proof introduces negations and removes none; the second removes one, at its $\mathrm{RAA}$ step. Which rule a “suppose not” uses is decided by the lines as written: what the box assumes, and what is written after it. Under the convention of Section 2.1 an order statement can be written either way: with the goal $x < 0$ written as $\neg(x \ge 0)$ , the box on $x \ge 0$ closes by $\mathrm{\neg I}$ ; and Example (A number whose square is at most itself), with its goal written $\neg(x > 1)$ and its box on $x > 1$ , would close by $\mathrm{\neg I}$ too.

The proof of Theorem 2.2.1 assumes the positive statement $r^2 = 2$ and concludes its negation, so it is $\mathrm{\neg I}$ .

Quick check. $\mathrm{\neg I}$ or $\mathrm{RAA}$ ? (i) “Suppose $15$ is prime. Then … This is a contradiction. Hence $15$ is not prime.” (ii) “Suppose $n$ is not odd. Then … This is a contradiction. Hence $n$ is odd.”

Solution.

(i) $\mathrm{\neg I}$ : the box opens with the statement whose negation is concluded. (ii) $\mathrm{RAA}$ : the box opens with $\neg$ ( $n$ is odd), and the conclusion is “ $n$ is odd”.

Second readingRAA is never needed to finish a negation

For one kind of goal the new rule is never needed at the last step. Suppose the goal is itself a negation $\neg\psi$ . An $\mathrm{RAA}$ box for it opens with $\neg\neg\psi$ . Replace it by a $\mathrm{\neg I}$ box that opens with $\psi$ ; inside it, derive $\neg\neg\psi$ from $\psi$ by the three lines of Example (Two negations from one premise) (a) (a box on $\neg\psi$ that clashes with $\psi$ ); then continue as the $\mathrm{RAA}$ box did, citing that line wherever the $\mathrm{RAA}$ box cited its assumption. The box still ends in $\bot$ , and $\mathrm{\neg I}$ closes it with $\neg\psi$ . So the last step of a derivation of a negation never needs $\mathrm{RAA}$ , though steps inside its box still may. $\mathrm{RAA}$ earns its place on the other goals.

When $Q$ is itself a negation, the inner goal in Proposition 2.5.2 is a negation, and its $\mathrm{RAA}$ can be replaced by $\mathrm{\neg I}$ in this way.

Warning. An $\mathrm{RAA}$ box on $\neg\varphi$ whose assumption is used only at its last step, against a $\varphi$ derived without it, is legal, but it is a direct proof in disguise: the lines before the clash already derive $\varphi$ , so the box can be deleted. The smallest case opens a box on $\neg P$ only to clash with a premise $P$ that is already the goal. It is a direct proof in costume. (A box that reaches $\bot$ without using its assumption at all is a different matter: the same lines, written before the box, derive $\bot$ without it, and $\mathrm{\bot E}$ then gives the goal at once.)

Warning. Not every “proof by contradiction” is $\mathrm{RAA}$ . Calling the proof of Theorem 2.2.1 an $\mathrm{RAA}$ is a mislabeling: its box opens with $r^2 = 2$ , not with a negation, and it concludes $r^2 \ne 2$ , which $\mathrm{\neg I}$ writes. The difference matters when you count classical steps: the box of that proof closes by $\mathrm{\neg I}$ and contributes none.

2.5.10. The rule card

Before the card, the new rule on large statements; each box runs from the assumption shown to $\bot$ .

Example (Instances of

\mathrm{RAA}

)

$\varphi$	The box opens with	New line
$P \vee \neg Q$	$\neg(P \vee \neg Q)$	$P \vee \neg Q$
$(P \to Q) \to R$	$\neg((P \to Q) \to R)$	$(P \to Q) \to R$
$\neg Q$	$\neg\neg Q$	$\neg Q$

The third row is legal; a $\mathrm{\neg I}$ box opened by $Q$ would also do (the fold “RAA is never needed to finish a negation”).

Not an instance. A box opens with $\neg P \vee \neg Q$ and reaches $\bot$ . The line “ $P \wedge Q$ — $\mathrm{RAA}$ ” is not an instance: the assumption must be $\neg(P \wedge Q)$ , the negation of the whole line written. $\neg P \vee \neg Q$ says the same only after a derivation (De Morgan’s laws), and the rule compares symbols.

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
$\mathrm{\neg E}$	$\varphi$ , $\neg\varphi$ $\Longrightarrow$ $\bot$	“…, which contradicts …”	`exact hn hp` (goal `False`)
$\mathrm{\bot E}$	$\bot$ $\Longrightarrow$ any $\varphi$	“This case cannot occur.” “So there is nothing to prove.”	`exfalso`
$\mathrm{\neg I}$	box $\varphi$ … $\bot$ $\Longrightarrow$ $\neg\varphi$	“Suppose $P$ . … This is a contradiction. Hence not $P$ .”	`intro hp` (goal `False`)
$\mathrm{MT}$ (derived)	$\varphi \to \psi$ , $\neg\psi$ $\Longrightarrow$ $\neg\varphi$	“Since $Q$ fails, so does $P$ .”	`mt h hnq`
$\mathrm{CP}$ (derived)	$\varphi \to \psi$ $\Longrightarrow$ $\neg\psi \to \neg\varphi$	“We prove the contrapositive: suppose not $Q$ ; … so not $P$ .”	`mt`
$\mathrm{DS}$ (derived)	$\varphi \vee \psi$ , $\neg\varphi$ $\Longrightarrow$ $\psi$	“ $P$ is impossible, so $Q$ .”	`h.resolve_left hnp`
$\mathrm{{\leftrightarrow}I}$	box $\varphi$ … $\psi$ , box $\psi$ … $\varphi$ $\Longrightarrow$ $\varphi \leftrightarrow \psi$	“ $(\Rightarrow)$ Suppose $P$ . … so $Q$ . $(\Leftarrow)$ Suppose $Q$ . … so $P$ .”	`constructor`
$\mathrm{{\leftrightarrow}E}$	$\varphi \leftrightarrow \psi$ , $\varphi$ $\Longrightarrow$ $\psi$ (or with $\psi$ , $\varphi$ )	“Since $P$ holds if and only if $Q$ does, and $P$ holds, so does $Q$ .”	`h.mp hp` / `h.mpr hq`
$\mathrm{RAA}$	box $\neg\varphi$ … $\bot$ $\Longrightarrow$ $\varphi$	“Suppose, for a contradiction, that $P$ fails. … This is impossible. Hence $P$ .”	`by_contra h`
$\mathrm{\neg\neg E}$ (derived)	$\neg\neg\varphi$ $\Longrightarrow$ $\varphi$	“It cannot be that $P$ fails; so $P$ .”	`not_not.mp h`
$\mathrm{LEM}$ (derived)	nothing $\Longrightarrow$ $\varphi \vee \neg\varphi$	“Either $P$ or not. If $P$ , … If not, … In either case, …”	`by_cases h : P`

The Lean column is for readers who use that proof assistant; nothing later depends on it.

Warning (Not allowed: $\mathrm{RAA}$ ). Each step is wrong; the tag names the clause it breaks.

Open the box for $Q \vee R$ with $\neg Q \vee R$ : clause 1, the box opens with the negation of the whole goal.
Write $\varphi$ after a box opened by $\varphi$ : clause 1 (the pair below).
Close the box on a $\bot$ of a box inside it: clause 2.
Write $\neg\neg\varphi$ by $\mathrm{RAA}$ : clause 3; $\neg\neg\varphi$ is the line $\mathrm{\neg I}$ writes.
To prove $x \le 1$ , assume $x \ge 1$ : clause 1, the negation of $x \le 1$ is $x > 1$ .

Clause 1 is where the rule bites. Premises $(P \vee R) \to Q$ and $\neg Q$ ; wrong on the left, right on the right:

(P \vee R) \to Q

\neg Q

P

asm, for

\mathrm{RAA}

P \vee R

\mathrm{{\vee}I}

Q

\mathrm{{{\to}}E}

1, 4

\bot

\mathrm{{\neg}E}

5, 2

P

\mathrm{RAA}

3–6

(P \vee R) \to Q

\neg Q

P

asm, for

\mathrm{{\neg}I}

P \vee R

\mathrm{{\vee}I}

Q

\mathrm{{{\to}}E}

1, 4

\bot

\mathrm{{\neg}E}

5, 2

\neg P

\mathrm{{\neg}I}

3–6

The left box opened with $P$ , not $\neg P$ , so it refuted $P$ and cannot conclude it. The claim $(P \vee R) \to Q, \ \neg Q \vdash P$ breaks: let $x$ be a real number, with $P$ : “ $x > 2$ ”, $R$ : “ $x < -2$ ”, $Q$ : “ $x^2 > 4$ ”. The first premise holds for every $x$ , and at $x = 0$ the second holds and $P$ fails.

Quick check. A box opens with $\neg(x \ne 2)$ , for a real number $x$ , and reaches $\bot$ as a line of the box itself. What may $\mathrm{RAA}$ write after it, and what may $\mathrm{\neg I}$ ?

Solution. $\mathrm{RAA}$ writes $x \ne 2$ ; $\mathrm{\neg I}$ writes $\neg\neg(x \ne 2)$ , that is $\neg\neg\neg(x = 2)$ .

Remark (Looking ahead). Chapter 4 proves that $P$ cannot be derived from $\neg\neg P$ , nor Peirce’s law from no premises, without $\mathrm{RAA}$ or one of its two equivalents, and states the same, without proof, for De Morgan’s law (d) and for $(P \to Q) \vee (Q \to P)$ . Chapter 8 tells the story of the mathematicians who declined the classical principle, and shows how to spot a proof by contradiction that is a direct proof in costume.

2.5.11. Exercises

A. Check your understanding

Exercise (A1)

(a) “Suppose $7$ is even. Then $7 = 2k$ for some integer $k$ , so $k = 7/2$ , which is not an integer. This is impossible. Hence $7$ is not even.” Is the last step $\mathrm{\neg I}$ , $\mathrm{RAA}$ , or neither? What did the box open with?
(b) “Let $x$ be real. Suppose $x^2 \ge 2x - 1$ fails, that is, $x^2 < 2x - 1$ . Then $(x - 1)^2 < 0$ , which is impossible. Hence $x^2 \ge 2x - 1$ .” Same questions.
(c) “Assume $P$ . Then, as shown above, $Q$ . Hence $P \to Q$ .” Same questions.
(d) State $\mathrm{RAA}$ and $\mathrm{\neg I}$ side by side, and say which of the two the derivation of Proposition 2.5.1 (a) uses.
(e) In the derivation of Proposition 2.5.5 (d), why is a last line $\mathrm{\vee I}$ , from $\neg P$ or $\neg Q$ derived from the premise alone, not worth aiming at?
(f) In the same derivation, the assumption $\neg(\neg P \vee \neg Q)$ on line 2 is cited twice. Name the two lines that cite it, and the rule each uses.
(g) In the instance of ② on the opening example (in “One principle in three forms”), which rule justifies the line $\neg\neg(x \le 1)$ , and why does the box of lines 2–5 need no change?

Solution.

(a) $\mathrm{\neg I}$ : the box opened with “ $7$ is even”, and the conclusion is its negation. ( $7/2$ is not an integer because $3 < 7/2 < 4$ .)
(b) $\mathrm{RAA}$ : the box opened with the negation of $x^2 \ge 2x - 1$ , and the conclusion is $x^2 \ge 2x - 1$ itself. (The clash: $x^2 < 2x - 1$ rearranges to $(x - 1)^2 < 0$ , and squares are nonnegative.)
(c) Neither: this is $\mathrm{{\to}I}$ . The box opened with $P$ and ended with $Q$ ; no $\bot$ appears.
(d) $\mathrm{\neg I}$ : a box that opens with $\varphi$ and reaches $\bot$ gives $\neg\varphi$ . $\mathrm{RAA}$ : a box that opens with $\neg\varphi$ and reaches $\bot$ gives $\varphi$ . The derivation of Proposition 2.5.1 (a) uses $\mathrm{\neg I}$ , with $\neg P$ as the assumption, so its conclusion is the negation of $\neg P$ , namely $\neg\neg P$ .
(e) $\mathrm{\vee I}$ would need $\neg P$ or $\neg Q$ on a line derived from the premise alone, and each of those steps can be broken: with $P$ true and $Q$ false the premise is true and $\neg P$ false, and with $P$ false and $Q$ true the premise is true and $\neg Q$ false. So neither step is worth aiming at: each breaks (Section 1.1’s test).
(f) Line 5 cites it, by $\mathrm{\neg E}$ against line 4, $\neg P \vee \neg Q$ ; and line 9 cites it, by $\mathrm{\neg E}$ against line 8, the same statement. Both lines lie in boxes inside the box of line 2, which is still open, so the citations are legal.
(g) $\mathrm{\neg I}$ : the box opens with $\neg(x \le 1)$ and ends with $\bot$ , so $\mathrm{\neg I}$ gives the negation of its assumption, $\neg\neg(x \le 1)$ . The box needs no change because $\mathrm{\neg I}$ , like $\mathrm{RAA}$ , asks only for a box that ends with $\bot$ as a line of the box itself; the two rules differ in what they write after the box, not in the box.

Exercise (A2: Drill)

The parts run from one step, through a missing line, a justification column and steps to judge, to short derivations.

(a) A box opens with $\neg(P \wedge Q)$ and ends with $\bot$ , a line of the box itself. What may $\mathrm{RAA}$ write after it, and what may $\mathrm{\neg I}$ ?
(b) Line 1 is $\neg\neg(P \to Q)$ . What does “ $\mathrm{\neg\neg E}$ 1” write?
(c) To prove $Q \vee R$ by $\mathrm{RAA}$ , which statement opens the box?
(d) Let $x$ be a real number. To prove $x \ge 2$ by contradiction, what is assumed?
(e) Line 9 is $P \to Q$ , justified “ $\mathrm{RAA}$ 4–8”. What are lines 4 and 8?
(f) Line 6 is $Q \vee R$ , justified “ $\mathrm{\neg\neg E}$ 5”. What is line 5, and by which rule is such a line usually written?
(g) Fill in the justifications (i)–(iv).

1 $\neg\neg (P \wedge Q)$
2 $Q \to R$
3 $P \wedge Q$ (i)
4 $Q$ (ii)
5 $R$ (iii)
6 $R \vee S$ (iv)
(h) “Suppose $9$ is prime. … This is impossible. Hence $9$ is not prime.” Is the last step $\mathrm{\neg I}$ or $\mathrm{RAA}$ ?
(i) “Suppose $n^2$ is not even. … This is impossible. Hence $n^2$ is even.” Is the last step $\mathrm{\neg I}$ or $\mathrm{RAA}$ ?
(j) Which of $\mathrm{\neg\neg I}$ , $\mathrm{\neg\neg E}$ , $\mathrm{LEM}$ , $\mathrm{MT}$ , $\mathrm{DS}$ are derived in this chapter by a derivation that uses $\mathrm{RAA}$ ?
(k) Find the illegal line, and say why it is illegal.

1 $\neg (P \wedge Q)$
2 $\neg P$ asm, for $\mathrm{RAA}$
3 $P \wedge Q$ asm, for $\mathrm{{\neg}I}$
4 $P$ $\mathrm{{\wedge}E}$ 3
5 $\bot$ $\mathrm{{\neg}E}$ 4, 2
6 $\neg (P \wedge Q)$ $\mathrm{{\neg}I}$ 3–5
7 $P$ $\mathrm{RAA}$ 2–5
(l) A box opens at line 2 with $\neg P$ ; line 4, a line of that box itself, is $\bot$ . Is “5. $\neg\neg P$ — $\mathrm{RAA}$ 2–4” correct?
(m) Derive $\neg\neg P, \ P \to Q \vdash Q$ .
(n) Derive $\neg P \to P \vdash P$ .
(o) Derive $\neg P \to Q, \ \neg Q \vdash P$ in two lines after the premises.

Solution.

(a) $\mathrm{RAA}$ writes $P \wedge Q$ ; $\mathrm{\neg I}$ writes $\neg\neg(P \wedge Q)$ .
(b) $P \to Q$ .
(c) $\neg(Q \vee R)$ , the negation of the whole goal; not $\neg Q \vee R$ .
(d) $x < 2$ , that is $\neg(x \ge 2)$ ; not $x \le 2$ , which $x = 2$ satisfies together with the goal.
(e) Line 4 is the assumption $\neg(P \to Q)$ , “asm, for $\mathrm{RAA}$ ”; line 8 is $\bot$ , the last line of the box.
(f) Line 5 is $\neg\neg(Q \vee R)$ . Such a line is usually written by $\mathrm{\neg I}$ , closing a box opened by $\neg(Q \vee R)$ (or it is a premise).
(g)
- (i) $\mathrm{\neg\neg E}$ 1; (ii) $\mathrm{\wedge E}$ 3; (iii) $\mathrm{{\to}E}$ 2, 4; (iv) $\mathrm{\vee I}$ 5.
(h) $\mathrm{\neg I}$ : the box opens with “ $9$ is prime”, and the conclusion is its negation.
(i) $\mathrm{RAA}$ : the box opens with the negation of “ $n^2$ is even”, and the conclusion is that statement itself.
(j) $\mathrm{\neg\neg E}$ and $\mathrm{LEM}$ ; $\mathrm{\neg\neg I}$ , $\mathrm{MT}$ and $\mathrm{DS}$ are derived without it.
(k) Line 7: lines 2–5 are not a box (the box opened at line 2 ends at line 6), and $\mathrm{RAA}$ needs $\bot$ as a line of the box itself.
(l) No: $\mathrm{RAA}$ writes $P$ , the statement whose negation opened the box (clause 3); $\neg\neg P$ is the line $\mathrm{\neg I}$ writes after the same box.
(m) 3 $P$ , $\mathrm{\neg\neg E}$ 1; 4 $Q$ , $\mathrm{{\to}E}$ 2, 3.
(n) 2 $\neg P$ , assumption, for $\mathrm{RAA}$ ; 3 $P$ , $\mathrm{{\to}E}$ 1, 2; 4 $\bot$ , $\mathrm{\neg E}$ 3, 2; 5 $P$ , $\mathrm{RAA}$ $2\text{–}4$ .
(o) 3 $\neg\neg P$ , $\mathrm{MT}$ 1, 2; 4 $P$ , $\mathrm{\neg\neg E}$ 3.

B. Practice

Exercise (B1: With and without the new rule, used later)

(a) Derive $\neg\neg P, \ \neg\neg(P \to Q) \vdash \neg\neg Q$ without $\mathrm{RAA}$ . Then say in one sentence why your derivation does not give $Q$ .
(b) Derive $\neg P \to Q, \ \neg P \to \neg Q \vdash P$ , using $\mathrm{RAA}$ .

Hint: in (a) the goal is a negation; in (b) it is a letter.

Solution.

(a) The goal $\neg\neg Q$ is a negation, so we open a $\mathrm{\neg I}$ box on $\neg Q$ , with the goal $\bot$ . The premises are negations, so each can only clash: $\neg\neg P$ against $\neg P$ , and $\neg\neg(P \to Q)$ against $\neg(P \to Q)$ . Both of those are negations, so each is itself a subgoal for a $\mathrm{\neg I}$ box. Make $\neg P$ the subgoal: a box on $P$ . Inside it, make $\neg(P \to Q)$ the subgoal: a box on $P \to Q$ , where $\mathrm{{\to}E}$ gives $Q$ , which clashes with $\neg Q$ . The boxes then close from the inside out.
1 $\neg\neg P$
2 $\neg\neg (P \to Q)$
3 $\neg Q$ asm, for $\mathrm{{\neg}I}$
4 $P$ asm, for $\mathrm{{\neg}I}$
5 $P \to Q$ asm, for $\mathrm{{\neg}I}$
6 $Q$ $\mathrm{{{\to}}E}$ 5, 4
7 $\bot$ $\mathrm{{\neg}E}$ 6, 3
8 $\neg (P \to Q)$ $\mathrm{{\neg}I}$ 5–7
9 $\bot$ $\mathrm{{\neg}E}$ 8, 2
10 $\neg P$ $\mathrm{{\neg}I}$ 4–9
11 $\bot$ $\mathrm{{\neg}E}$ 10, 1
12 $\neg\neg Q$ $\mathrm{{\neg}I}$ 3–11

All three boxes close by $\mathrm{\neg I}$ , so no $\mathrm{RAA}$ is used. The derivation does not give $Q$ because its last box opens with $\neg Q$ , and $\mathrm{\neg I}$ can only write the negation of that assumption, $\neg\neg Q$ ; removing the two negations is $\mathrm{\neg\neg E}$ , a classical step.
(b) The goal $P$ is a letter, and both premises want $\neg P$ , which is nowhere. We are stuck, so we open an $\mathrm{RAA}$ box with $\neg P$ , and it feeds both premises:

\neg P \to Q

\neg P \to \neg Q

\neg P

asm, for

\mathrm{RAA}

Q

\mathrm{{{\to}}E}

1, 3

\neg Q

\mathrm{{{\to}}E}

2, 3

\bot

\mathrm{{\neg}E}

4, 5

P

\mathrm{RAA}

3–6

In words: “Suppose, for a contradiction, that $P$ fails. Then the premises give both $Q$ and $\neg Q$ , which is impossible. Hence $P$ .”

Exercise (B2: Back from negated sides, used later)

Derive $\neg P \leftrightarrow \neg Q \vdash P \leftrightarrow Q$ . Say where $\mathrm{RAA}$ enters and why.

Solution. The goal is a biconditional, so by Definition 2.4.1 we need two boxes, one from $P$ to $Q$ and one from $Q$ to $P$ . In the first, the goal $Q$ is a letter and the premise speaks only about $\neg Q$ , so we are stuck: we assume $\neg Q$ and argue by $\mathrm{RAA}$ . The second box is symmetric.

\neg P \leftrightarrow \neg Q

P

asm, for

\mathrm{{{\leftrightarrow}}I}

\neg Q

asm, for

\mathrm{RAA}

\neg P

\mathrm{{{\leftrightarrow}}E}

1, 3

\bot

\mathrm{{\neg}E}

2, 4

Q

\mathrm{RAA}

3–5

Q

asm, for

\mathrm{{{\leftrightarrow}}I}

\neg P

asm, for

\mathrm{RAA}

\neg Q

\mathrm{{{\leftrightarrow}}E}

1, 8

\bot

\mathrm{{\neg}E}

7, 9

P

\mathrm{RAA}

8–10

P \leftrightarrow Q

\mathrm{{{\leftrightarrow}}I}

2–6, 7–11

$\mathrm{RAA}$ enters at lines 6 and 11: each inner goal is a letter, and the premise produces only negations. In the converse, $P \leftrightarrow Q \vdash \neg P \leftrightarrow \neg Q$ (Example (Negating both sides of an iff)), the inner goals are negations, $\mathrm{\neg I}$ builds them, and no $\mathrm{RAA}$ is used.

Exercise (B3: The redundant rule)

Show that $\mathrm{\bot E}$ is derivable from $\mathrm{RAA}$ and repetition: given a line $\bot$ , derive an arbitrary statement $P$ in one box, without $\mathrm{\bot E}$ .

Solution. Open an $\mathrm{RAA}$ box with $\neg P$ and repeat the $\bot$ inside it:

\bot

\neg P

asm, for

\mathrm{RAA}

\bot

\mathrm{R}

P

\mathrm{RAA}

2–3

The repetition at line 3 is needed because $\mathrm{RAA}$ asks for $\bot$ as a line of the box itself. So every use of $\mathrm{\bot E}$ can be replaced by these three lines; the book keeps the rule for the reason given in the remark after Theorem 2.5.7.

Exercise (B4: Stuck at a letter)

A search for $(\neg P \to Q) \wedge (\neg P \to R), \ \neg(Q \wedge R) \vdash P$ has reached the stage below. Name the move, then complete it.

(\neg P \to Q) \wedge (\neg P \to R)

\neg (Q \wedge R)

\vdots

P

Solution. The goal $P$ is a letter, so no introduction rule applies, and both halves of the first premise wait for $\neg P$ , which is nowhere. The move is when stuck, assume the negation of the goal: open an $\mathrm{RAA}$ box on $\neg P$ , and hunt for a clash. The assumption feeds both halves, and $Q \wedge R$ then clashes with the second premise.

(\neg P \to Q) \wedge (\neg P \to R)

\neg (Q \wedge R)

\neg P

asm, for

\mathrm{RAA}

\neg P \to Q

\mathrm{{\wedge}E}

Q

\mathrm{{{\to}}E}

4, 3

\neg P \to R

\mathrm{{\wedge}E}

R

\mathrm{{{\to}}E}

6, 3

Q \wedge R

\mathrm{{\wedge}I}

5, 7

\bot

\mathrm{{\neg}E}

8, 2

P

\mathrm{RAA}

3–9

The assumption on line 3 is cited twice, at lines 5 and 7; the clash on line 9 is between a line built from it and the second premise.

Exercise (B5: Derive or break, used later)

For each claim, derive it with any of the rules of Chapters 1 and 2, or break it by statements about a real number $x$ . In each derivation, mark the classical line ( $\mathrm{RAA}$ , or $\mathrm{\neg\neg E}$ or $\mathrm{LEM}$ used as a derived rule), if there is one. (A derivation by $\mathrm{RAA}$ of $\Gamma \vdash \varphi$ derives $\bot$ from $\Gamma$ together with $\neg\varphi$ : from the counterexample set of the claim, Definition 1.1.3.)

(a) $P \vee Q, \ \neg P \vee R \vdash Q \vee R$ .
(b) $\neg(P \wedge Q) \vdash \neg P \wedge \neg Q$ .
(c) $P \to Q \vdash (P \leftrightarrow Q) \vee Q$ .
(d) $(P \to Q) \vee (P \to R) \vdash P \to (Q \wedge R)$ .
(e) $\neg\neg P \vee Q \vdash P \vee Q$ .
(f) $\neg(P \leftrightarrow Q) \vdash P \leftrightarrow \neg Q$ .
(g) $\neg(P \leftrightarrow Q) \vdash \neg P \wedge Q$ .
(h) $(P \wedge Q) \to R \vdash (P \to R) \vee (Q \to R)$ .

Solution.

(a) Derive, with no classical line. Split on the first premise; in the case $P$ , split on the second, where the case $\neg P$ closes itself.
1 $P \vee Q$
2 $\neg P \vee R$
3 $P$ asm, for $\mathrm{{\vee}E}$
4 $\neg P$ asm, for $\mathrm{{\vee}E}$
5 $\bot$ $\mathrm{{\neg}E}$ 3, 4
6 $Q \vee R$ $\mathrm{{\bot}E}$ 5
7 $R$ asm, for $\mathrm{{\vee}E}$
8 $Q \vee R$ $\mathrm{{\vee}I}$ 7
9 $Q \vee R$ $\mathrm{{\vee}E}$ 2, 4–6, 7–8
10 $Q$ asm, for $\mathrm{{\vee}E}$
11 $Q \vee R$ $\mathrm{{\vee}I}$ 10
12 $Q \vee R$ $\mathrm{{\vee}E}$ 1, 3–9, 10–11
(b) Break. Take $P$ : “ $x > 0$ ”, $Q$ : “ $x > 5$ ”. At $x = 1$ , $P \wedge Q$ is false, so $\neg(P \wedge Q)$ is true, and $\neg P$ is false, so $\neg P \wedge \neg Q$ is false: the counterexample set $\neg(P \wedge Q)$ , $\neg(\neg P \wedge \neg Q)$ is true. This is the wrong De Morgan law.
(c) Derive; the classical line is line 2, $\mathrm{LEM}$ (Proposition 2.5.3 as a derived rule). Each side of the goal breaks on its own: with $P$ : “ $x > 5$ ”, $Q$ : “ $x > 3$ ”, the premise holds at every $x$ , $P \leftrightarrow Q$ fails at $x = 4$ and $Q$ at $x = 0$ . So decide a letter first. The letter is $Q$ : in the case $Q$ the right side is in hand, and in the case $\neg Q$ the premise and the clash with $\neg Q$ build $P \leftrightarrow Q$ in two boxes.

1 $P \to Q$
2 $Q \vee \neg Q$ $\mathrm{LEM}$
3 $Q$ asm, for $\mathrm{{\vee}E}$
4 $(P \leftrightarrow Q) \vee Q$ $\mathrm{{\vee}I}$ 3
5 $\neg Q$ asm, for $\mathrm{{\vee}E}$
6 $P$ asm, for $\mathrm{{{\leftrightarrow}}I}$
7 $Q$ $\mathrm{{{\to}}E}$ 1, 6
8 $Q$ asm, for $\mathrm{{{\leftrightarrow}}I}$
9 $\bot$ $\mathrm{{\neg}E}$ 8, 5
10 $P$ $\mathrm{{\bot}E}$ 9
11 $P \leftrightarrow Q$ $\mathrm{{{\leftrightarrow}}I}$ 6–7, 8–10
12 $(P \leftrightarrow Q) \vee Q$ $\mathrm{{\vee}I}$ 11
13 $(P \leftrightarrow Q) \vee Q$ $\mathrm{{\vee}E}$ 2, 3–4, 5–12

Deciding $P$ first, as the Idea of Proposition 2.5.6 (b) does, would leave the case $\neg P$ with neither side in hand.
(d) Break. Take $P$ : “ $x > 0$ ”, $Q$ : “ $x > -1$ ”, $R$ : “ $x > 5$ ”. At $x = 1$ , $P \to Q$ is true, so the premise is, and $Q \wedge R$ is false while $P$ is true, so $P \to (Q \wedge R)$ is false: the counterexample set is true.
(e) Derive; the classical line is line 3, $\mathrm{\neg\neg E}$ .

1 $\neg\neg P \vee Q$
2 $\neg\neg P$ asm, for $\mathrm{{\vee}E}$
3 $P$ $\mathrm{{\neg\neg}E}$ 2
4 $P \vee Q$ $\mathrm{{\vee}I}$ 3
5 $Q$ asm, for $\mathrm{{\vee}E}$
6 $P \vee Q$ $\mathrm{{\vee}I}$ 5
7 $P \vee Q$ $\mathrm{{\vee}E}$ 1, 2–4, 5–6
(f) Derive; the classical line is line 21, $\mathrm{RAA}$ . The goal is a biconditional, so two boxes. In the first, $\neg Q$ is a negation and $\mathrm{\neg I}$ builds it; in the second, the goal $P$ is a letter, and an $\mathrm{RAA}$ box on $\neg P$ gives the clash.
1 $\neg (P \leftrightarrow Q)$
2 $P$ asm, for $\mathrm{{{\leftrightarrow}}I}$
3 $Q$ asm, for $\mathrm{{\neg}I}$
4 $P$ asm, for $\mathrm{{{\leftrightarrow}}I}$
5 $Q$ $\mathrm{R}$ 3
6 $Q$ asm, for $\mathrm{{{\leftrightarrow}}I}$
7 $P$ $\mathrm{R}$ 2
8 $P \leftrightarrow Q$ $\mathrm{{{\leftrightarrow}}I}$ 4–5, 6–7
9 $\bot$ $\mathrm{{\neg}E}$ 8, 1
10 $\neg Q$ $\mathrm{{\neg}I}$ 3–9
11 $\neg Q$ asm, for $\mathrm{{{\leftrightarrow}}I}$
12 $\neg P$ asm, for $\mathrm{RAA}$
13 $P$ asm, for $\mathrm{{{\leftrightarrow}}I}$
14 $\bot$ $\mathrm{{\neg}E}$ 13, 12
15 $Q$ $\mathrm{{\bot}E}$ 14
16 $Q$ asm, for $\mathrm{{{\leftrightarrow}}I}$
17 $\bot$ $\mathrm{{\neg}E}$ 16, 11
18 $P$ $\mathrm{{\bot}E}$ 17
19 $P \leftrightarrow Q$ $\mathrm{{{\leftrightarrow}}I}$ 13–15, 16–18
20 $\bot$ $\mathrm{{\neg}E}$ 19, 1
21 $P$ $\mathrm{RAA}$ 12–20
22 $P \leftrightarrow \neg Q$ $\mathrm{{{\leftrightarrow}}I}$ 2–10, 11–21
(g) Break. Take $P$ : “ $x > 0$ ”, $Q$ : “ $x > 5$ ”. At $x = 1$ , $P$ is true and $Q$ false, so $P \leftrightarrow Q$ is false and the premise is true; $\neg P$ is false, so $\neg P \wedge Q$ is false.
(h) Derive; the classical line is line 14, $\mathrm{RAA}$ . Each side of the goal breaks on its own: with $P$ : “ $x > 0$ ”, $Q$ : “ $x > 5$ ”, $R$ : “ $x > 3$ ”, the premise holds at every $x$ and $P \to R$ fails at $x = 1$ ; exchanging the statements for $P$ and $Q$ breaks the step to $Q \to R$ at the same $x$ . So assume the negation of the whole goal. Inside, the box on $P$ turns the clash into $R$ , and the box on $Q$ inside it builds $P \wedge Q$ .

(P \wedge Q) \to R

\neg ((P \to R) \vee (Q \to R))

asm, for

\mathrm{RAA}

P

asm, for

\mathrm{{{\to}}I}

Q

asm, for

\mathrm{{{\to}}I}

P \wedge Q

\mathrm{{\wedge}I}

3, 4

R

\mathrm{{{\to}}E}

1, 5

Q \to R

\mathrm{{{\to}}I}

4–6

(P \to R) \vee (Q \to R)

\mathrm{{\vee}I}

\bot

\mathrm{{\neg}E}

8, 2

R

\mathrm{{\bot}E}

P \to R

\mathrm{{{\to}}I}

3–10

(P \to R) \vee (Q \to R)

\mathrm{{\vee}I}

\bot

\mathrm{{\neg}E}

12, 2

(P \to R) \vee (Q \to R)

\mathrm{RAA}

2–13

(a) needs no classical line, although its goal is a disjunction, because each case of the premise hands over one side. (c) and (h) are disjunctions whose sides break on their own, the place “When $\mathrm{RAA}$ earns its place” points to, and the answers use both classical tools there: (c) decides a letter first with $\mathrm{LEM}$ , as Proposition 2.5.6 (b) does, but the letter is $Q$ , a side of the goal, not $P$ ; (h) assumes the negation of the goal. In (f) the classical line closes a box whose goal is a letter, $P$ from $\neg Q$ , as in Proposition 2.5.1, the other case that paragraph names; the box $2\text{–}10$ of (f) has no classical line. (b), (d) and (g) are look-alikes. Worked examples of these types: Proposition 2.5.3, Proposition 2.5.5 (d), Proposition 2.5.6 (b), Proposition 2.5.2.

Marking scheme. (16 points) For each claim: 1 for the verdict; 1 for a derivation every line of which checks, with the classical line correctly marked, 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 a premise fails; a classical line not marked, or a non-classical line marked as classical.

Exercise (B6: A law that sounds false)

(a) Show that $(P \to Q) \vee (Q \to P)$ cannot be broken: whatever statements $P$ and $Q$ are, one disjunct is true.
(b) Let $n$ be an integer, $P$ : “ $n$ is even”, $Q$ : “ $n > 5$ ”. Check the statement at $n = 2$ and at $n = 7$ , saying which disjunct holds.
(c) The sentence “every even integer is greater than $5$ , or every integer greater than $5$ is even” is false. Why is that no counterexample to (a)?
(d) Show that each disjunct, as a claim from no premises, breaks. Which move of this section does a derivation of $(P \to Q) \vee (Q \to P)$ then call for?

Solution.

(a) If $P$ is false, $P \to Q$ is true, since its hypothesis fails. If $P$ is true, $Q \to P$ is true, since its conclusion holds. Either way one disjunct is true.
(b) At $n = 2$ : $P$ is true and $Q$ false, so $Q \to P$ holds (and $P \to Q$ fails). At $n = 7$ : $P$ is false and $Q$ true, so $P \to Q$ holds (and $Q \to P$ fails).
(c) The false sentence puts “every” in front of each disjunct separately: (for every $n$ , $P \to Q$ ) or (for every $n$ , $Q \to P$ ). The value $n = 2$ refutes the first and $n = 7$ the second. What (a) gives is, for each $n$ , the disjunction itself, as (b) checked at two values. “Every” does not pass inside an “or”. This is the point of “Two sequents that sound wrong” in Section 2.1: the mathematical “if” sits under an “every”.
(d) $P \to Q$ breaks with $P$ : “ $x > 0$ ”, $Q$ : “ $x > 5$ ”, at $x = 1$ ; $Q \to P$ breaks with the same two statements exchanged, at $x = 1$ . So $\mathrm{\vee I}$ from either side is not worth aiming at, and the goal is a disjunction with neither side within reach: the case of “When $\mathrm{RAA}$ earns its place”, and the move when stuck, assume the negation of the goal. (The derivation itself is Exercise C2 of Section 3.1, where the search method finds it; Chapter 4 states, without proof, that every derivation of it uses $\mathrm{RAA}$ or one of its equivalents.)

Marking scheme. (10 points) 3: (a), both cases. 2: (b), the disjunct that holds at each value. 3: (c), the scope of “every” named, with a refuting value for each separated disjunct. 2: (d), the two breaks and the move named. Fatal error (0 for (c)): calling the false sentence an instance of (a).

C. Going deeper

Exercise (C1: Challenge: Excluded middle does the work of reductio directly)

Suppose that, instead of $\mathrm{RAA}$ , we had $\mathrm{LEM}$ as a rule: $\varphi \vee \neg\varphi$ may be written on any line, for any statement $\varphi$ .

Given a box that opens with $\neg\varphi$ and reaches $\bot$ , derive $\varphi$ using $\mathrm{LEM}$ , $\mathrm{\vee E}$ , $\mathrm{\bot E}$ , and the other primitive rules, but neither $\mathrm{RAA}$ nor $\mathrm{\neg\neg E}$ . Write the case $\neg\varphi$ as the given box, extended.

Solution (Hint 1). Write $\varphi \vee \neg\varphi$ just before the given box. What must each of the two case boxes end with?

Solution (Hint 2). The first case box is a single line.

Solution. Write excluded middle for $\varphi$ just before the given box, and use the box as the second case of $\mathrm{\vee E}$ , extended by one line:

h

\varphi \vee \neg \varphi

\mathrm{LEM}

h+1

\varphi

asm, for

\mathrm{{\vee}E}

i

\neg \varphi

asm, for

\mathrm{{\vee}E}

\vdots

j

\bot

j+1

\varphi

\mathrm{{\bot}E}

j

k

\varphi

\mathrm{{\vee}E}

h

h+1

–

h+1

i

–

j+1

Here $i = h + 2$ . The first case is a one-line box that already ends with the goal. The second case is the given box with one more line, $\mathrm{\bot E}$ on its $\bot$ ; its lines are unchanged and cite what they cited before, since the box has not moved into or out of any other box. No $\mathrm{RAA}$ and no $\mathrm{\neg\neg E}$ is used.

Exercise (C2: Find the error, used later)

A student derives $\neg(\neg P \wedge \neg Q) \vdash P \vee Q$ as follows.

\neg (\neg P \wedge \neg Q)

P \vee \neg P

\mathrm{LEM}

P

asm, for

\mathrm{{\vee}E}

P \vee Q

\mathrm{{\vee}I}

\neg P

asm, for

\mathrm{{\vee}E}

\bot

\mathrm{{\neg}E}

3, 5

Q

\mathrm{{\bot}E}

P \vee Q

\mathrm{{\vee}I}

P \vee Q

\mathrm{{\vee}E}

2, 3–4, 5–8

(a) Is the sequent $\neg(\neg P \wedge \neg Q) \vdash P \vee Q$ derivable?
(b) Does the student’s derivation derive it? Name the first line that fails and the rule or clause it breaks.
(c) Show that the illegal step, if it were allowed, would prove too much: use the same move to “derive” $P \vee Q \vdash P$ , and break that sequent.
(d) Give a correct derivation.

Solution.

(a) Yes: part (d) below gives a derivation. The conclusion is true, and the argument is still wrong.
(b) No. Line 6 fails: it cites line 3, the assumption of the first case box, lines 3–4, which closed before line 5. By the scope rule of Definition 1.4.2, line 3 is not available at line 6. The form of $\mathrm{\neg E}$ is right; what is broken is availability. In words, the student used the assumption of one case inside the other case, where it has not been assumed.
(c) The same move derives $P \vee Q \vdash P$ : split on the premise by $\mathrm{\vee E}$ , with a first box that opens with $P$ and ends there, and a second box that opens with $Q$ and “repeats” $P$ from the first. That sequent breaks: with $P$ false and $Q$ true the premise is true and the conclusion false, so the move can carry a true premise to a false conclusion. So citing a line of a sibling box is illegal in general, not just unlucky here.
(d) Keep lines 1–5, and in the case $\neg P$ we are stuck at the goal $Q$ , so we argue for it by $\mathrm{RAA}$ , using the premise:

\neg (\neg P \wedge \neg Q)

P \vee \neg P

\mathrm{LEM}

P

asm, for

\mathrm{{\vee}E}

P \vee Q

\mathrm{{\vee}I}

\neg P

asm, for

\mathrm{{\vee}E}

\neg Q

asm, for

\mathrm{RAA}

\neg P \wedge \neg Q

\mathrm{{\wedge}I}

5, 6

\bot

\mathrm{{\neg}E}

7, 1

Q

\mathrm{RAA}

6–8

P \vee Q

\mathrm{{\vee}I}

P \vee Q

\mathrm{{\vee}E}

2, 3–4, 5–10

Line 7 cites line 5, the assumption of the enclosing case box, which is still open: the legal version of what the student wanted.

Exercise (C3: Exit check: a classical disjunction)

Derive $\vdash P \vee (P \to Q)$ using the primitive rules only (those of Chapter 1, $\mathrm{\neg E}$ , $\mathrm{\bot E}$ , $\mathrm{\neg I}$ , $\mathrm{{\leftrightarrow}I}$ , $\mathrm{{\leftrightarrow}E}$ , and $\mathrm{RAA}$ ), with no derived rule, so neither $\mathrm{LEM}$ nor $\mathrm{\neg\neg E}$ as a single line. Name the rule on every line, and say which line is classical.

Solution. The search. The goal is a disjunction, so we postpone it; there are no premises, so no premise-directed move applies; and neither side is worth aiming at: $P$ false breaks the step to $P$ , and $P$ true with $Q$ false breaks the step to $P \to Q$ . We are stuck, so we assume the exact negation of the goal, $\neg(P \vee (P \to Q))$ , and hunt for a clash. The assumption can clash only with $P \vee (P \to Q)$ , which $\mathrm{\vee I}$ builds from either side. The side $P \to Q$ is an implication, so we open a box on $P$ with the goal $Q$ . Inside it, $\mathrm{\vee I}$ gives $P \vee (P \to Q)$ from $P$ , which clashes with the assumption, and $\mathrm{\bot E}$ writes $Q$ . So $P \to Q$ holds, $\mathrm{\vee I}$ gives the goal, and that is the second clash.

\neg (P \vee (P \to Q))

asm, for

\mathrm{RAA}

P

asm, for

\mathrm{{{\to}}I}

P \vee (P \to Q)

\mathrm{{\vee}I}

\bot

\mathrm{{\neg}E}

3, 1

Q

\mathrm{{\bot}E}

P \to Q

\mathrm{{{\to}}I}

2–5

P \vee (P \to Q)

\mathrm{{\vee}I}

\bot

\mathrm{{\neg}E}

7, 1

P \vee (P \to Q)

\mathrm{RAA}

1–8

Lines 1 and 2 are assumptions, of the $\mathrm{RAA}$ box and of the $\mathrm{{\to}I}$ box; every other line names its rule on the right. The classical line is line 9; every other rule used is a rule for a connective. The shape is that of Proposition 2.5.3: there the inner box closed by $\mathrm{\neg I}$ to give $\neg P$ ; here it ends with $\mathrm{\bot E}$ and closes by $\mathrm{{\to}I}$ to give $P \to Q$ .

A second correct route first derives $P \vee \neg P$ by the eight lines of Proposition 2.5.3, written out, and then splits on it: in the case $P$ , $\mathrm{\vee I}$ gives the goal; in the case $\neg P$ , a box on $P$ clashes with $\neg P$ , $\mathrm{\bot E}$ writes $Q$ , $\mathrm{{\to}I}$ gives $P \to Q$ , and $\mathrm{\vee I}$ the goal. Its classical line is the $\mathrm{RAA}$ inside the written-out excluded middle.

Marking scheme. (10 points)

2: an $\mathrm{RAA}$ box opened with $\neg(P \vee (P \to Q))$ , the exact negation of the goal.
3: an inner box on $P$ that reaches $\bot$ by $\mathrm{\vee I}$ and $\mathrm{\neg E}$ against the outer assumption, and then $Q$ by $\mathrm{\bot E}$ .
2: $P \to Q$ by $\mathrm{{\to}I}$ , then $P \vee (P \to Q)$ by $\mathrm{\vee I}$ , and the second clash.
2: $\mathrm{RAA}$ closes the outer box, and it is named as the classical step.
1: every citation is available.

The second route earns the same points, step for step: 2 for the written-out excluded middle opened correctly (its $\mathrm{RAA}$ box on $\neg(P \vee \neg P)$ ); 3 for the box on $P$ in the case $\neg P$ , ending with $Q$ by $\mathrm{\bot E}$ ; 2 for $\mathrm{{\to}I}$ , the two $\mathrm{\vee I}$ lines, and the $\mathrm{\vee E}$ ; 2 for naming the $\mathrm{RAA}$ inside excluded middle as the classical step; 1 for availability. Fatal errors (0 for the step): opening the outer box with anything but $\neg(P \vee (P \to Q))$ ; closing the outer box by $\mathrm{\neg I}$ (that gives $\neg\neg(P \vee (P \to Q))$ ); a line justified by $\mathrm{\neg\neg E}$ or $\mathrm{LEM}$ taken as a rule, which the item excludes.

Exercise (C4: Challenge: Smaller rule sets)

(a) Show that, once $\mathrm{RAA}$ is a rule, $\mathrm{\neg I}$ could be dropped: given a box that opens with $\varphi$ and reaches $\bot$ as a line of its own, derive $\neg\varphi$ with $\mathrm{RAA}$ , $\mathrm{\neg E}$ and the box’s lines, without $\mathrm{\neg I}$ . Use your method to derive Proposition 2.3.1 without $\mathrm{\neg I}$ .
(b) With neither $\mathrm{\bot E}$ nor $\mathrm{RAA}$ ( $\mathrm{\neg I}$ allowed), derive $\neg P \vdash P \to \neg Q$ .
(c) Exercise B3 derived $\mathrm{\bot E}$ from $\mathrm{RAA}$ and repetition. Does its derivation use $\mathrm{\neg I}$ , and does your fragment in (a) use $\mathrm{\bot E}$ ? What do (a) and B3 together say about the list of thirteen primitive rules?
(d) Which of the two paradoxes of Section 2.1 survives in a system with neither $\mathrm{\bot E}$ nor $\mathrm{RAA}$ , by the derivation given there?

Solution.

(a) Replace the old box by this one. Line $i$ : $\neg\neg\varphi$ , assumption, for $\mathrm{RAA}$ . Line $i + 1$ : $\neg\varphi$ , assumption, for $\mathrm{RAA}$ . Line $i + 2$ : $\bot$ , $\mathrm{\neg E}$ $i + 1$ , $i$ . Line $i + 3$ : $\varphi$ , $\mathrm{RAA}$ $i+1\text{–}i+2$ . Then the old box’s lines after its assumption, renumbered, each citation of the old assumption now citing line $i + 3$ ; the last of them is $\bot$ , a line of the new box. Then $\neg\varphi$ , by $\mathrm{RAA}$ on the new box: $\mathrm{RAA}$ writes $\psi$ from a box opened by $\neg\psi$ , here with $\psi$ the statement $\neg\varphi$ . Every old citation stays available: the old lines sit in the new box exactly as they sat in the old one, and line $i + 3$ is a line of that box.
For modus tollens:

1 $P \to Q$
2 $\neg Q$
3 $\neg\neg P$ asm, for $\mathrm{RAA}$
4 $\neg P$ asm, for $\mathrm{RAA}$
5 $\bot$ $\mathrm{{\neg}E}$ 4, 3
6 $P$ $\mathrm{RAA}$ 4–5
7 $Q$ $\mathrm{{{\to}}E}$ 1, 6
8 $\bot$ $\mathrm{{\neg}E}$ 7, 2
9 $\neg P$ $\mathrm{RAA}$ 3–8
(b) A box on $P$ , and inside it a box on $Q$ whose $\bot$ comes from the clash of $P$ with the premise:
1 $\neg P$
2 $P$ asm, for $\mathrm{{{\to}}I}$
3 $Q$ asm, for $\mathrm{{\neg}I}$
4 $\bot$ $\mathrm{{\neg}E}$ 2, 1
5 $\neg Q$ $\mathrm{{\neg}I}$ 3–4
6 $P \to \neg Q$ $\mathrm{{{\to}}I}$ 2–5

The $\mathrm{\neg I}$ box never uses its assumption; the fold “Edge cases of not-introduction” of Section 2.2 explains why that is legal: the lines above it, $P$ and $\neg P$ , already clash.
(c) No, and no: B3 uses $\mathrm{RAA}$ and repetition only, and (a) uses $\mathrm{RAA}$ and $\mathrm{\neg E}$ only. So $\mathrm{\bot E}$ and $\mathrm{\neg I}$ can be dropped together, and the remaining eleven rules derive every sequent the thirteen do (replace the lines one at a time, innermost boxes first). The book keeps both for the reason the remark after Theorem 2.5.7 gives for $\mathrm{\bot E}$ : the primitive rules other than $\mathrm{RAA}$ are to form a system of their own.
(d) $Q \vdash P \to Q$ : its derivation uses $\mathrm{{\to}I}$ and repetition only. The derivation of $\neg P \vdash P \to Q$ given in Section 2.1 uses $\mathrm{\bot E}$ .

Marking scheme. (10 points) 5: (a), the general replacement (2 for the inner $\mathrm{RAA}$ producing $\varphi$ ; 1 for re-citing the old assumption; 1 for closing by $\mathrm{RAA}$ with $\psi$ the statement $\neg\varphi$ ) and 1 for the modus tollens derivation. 2: (b). 2: (c), both answers and the conclusion about the list. 1: (d). Fatal error (0 for (a)): closing the new box by $\mathrm{\neg I}$ , or opening it with $\varphi$ .

R. Review

Exercise (R1)

Let $n$ be an integer. Prove that $n^2 + 3n$ is even, naming the rule at each logical step.

Solution. By (E1), $n$ is even or $n$ is odd, and we argue by cases $[\mathrm{\vee E}]$ .

Case $n$ even. Write $n = 2k$ with $k$ an integer. Then $n^2 + 3n = 4k^2 + 6k = 2(2k^2 + 3k)$ , which is even.

Case $n$ odd. Write $n = 2k + 1$ with $k$ an integer. Then $n^2 + 3n = (4k^2 + 4k + 1) + (6k + 3) = 2(2k^2 + 5k + 2)$ , which is even.

Both cases reach the goal, so $n^2 + 3n$ is even $[\mathrm{\vee E}]$ .

The method is Chapter 1’s case split (Definition 1.6.1), used as in Example (The absolute value of a product), here on the parity of $n$ . No rule of this chapter is needed: neither case clashes, and each ends in the goal.

Exercise (R2)

Call an integer $n$ balanced if $n$ is even exactly when $n$ is a multiple of $3$ . Write $E$ : “ $n$ is even”, $T$ : “ $n$ is a multiple of $3$ ”.

(a) Write “ $n$ is balanced” in $E$ and $T$ , and decide it for $n = 4, 6, 7, 9$ .
(b) Show that “ $n$ is balanced” says the same as “ $n$ is both even and a multiple of $3$ , or neither”, by deriving $E \leftrightarrow T \dashv\vdash (E \wedge T) \vee (\neg E \wedge \neg T)$ . In which direction does your derivation use a classical line ( $\mathrm{RAA}$ , $\mathrm{\neg\neg E}$ or $\mathrm{LEM}$ )?

Solution.

(a) $E \leftrightarrow T$ : a definition’s “if” is read as an iff (Section 2.4, as in Example (A definition used in both directions); the rules are Definition 2.4.1). At $4$ , $E$ is true and $T$ false: not balanced. At $6$ , both are true: balanced. At $7$ , both are false: balanced. At $9$ , $E$ is false and $T$ true: not balanced.
(b) Left to right; the classical line is line 2, $\mathrm{LEM}$ (Proposition 2.5.3 as a derived rule):

E \leftrightarrow T

E \vee \neg E

\mathrm{LEM}

E

asm, for

\mathrm{{\vee}E}

T

\mathrm{{{\leftrightarrow}}E}

1, 3

E \wedge T

\mathrm{{\wedge}I}

3, 4

(E \wedge T) \vee (\neg E \wedge \neg T)

\mathrm{{\vee}I}

\neg E

asm, for

\mathrm{{\vee}E}

T

asm, for

\mathrm{{\neg}I}

E

\mathrm{{{\leftrightarrow}}E}

1, 8

\bot

\mathrm{{\neg}E}

9, 7

\neg T

\mathrm{{\neg}I}

8–10

\neg E \wedge \neg T

\mathrm{{\wedge}I}

7, 11

(E \wedge T) \vee (\neg E \wedge \neg T)

\mathrm{{\vee}I}

(E \wedge T) \vee (\neg E \wedge \neg T)

\mathrm{{\vee}E}

2, 3–6, 7–13

Right to left, with no classical line:

(E \wedge T) \vee (\neg E \wedge \neg T)

E \wedge T

asm, for

\mathrm{{\vee}E}

E

asm, for

\mathrm{{{\leftrightarrow}}I}

T

\mathrm{{\wedge}E}

T

asm, for

\mathrm{{{\leftrightarrow}}I}

E

\mathrm{{\wedge}E}

E \leftrightarrow T

\mathrm{{{\leftrightarrow}}I}

3–4, 5–6

\neg E \wedge \neg T

asm, for

\mathrm{{\vee}E}

E

asm, for

\mathrm{{{\leftrightarrow}}I}

\neg E

\mathrm{{\wedge}E}

\bot

\mathrm{{\neg}E}

9, 10

T

\mathrm{{\bot}E}

T

asm, for

\mathrm{{{\leftrightarrow}}I}

\neg T

\mathrm{{\wedge}E}

\bot

\mathrm{{\neg}E}

13, 14

E

\mathrm{{\bot}E}

E \leftrightarrow T

\mathrm{{{\leftrightarrow}}I}

9–12, 13–16

E \leftrightarrow T

\mathrm{{\vee}E}

1, 2–7, 8–17

The classical line of these derivations is in the left-to-right direction, the $\mathrm{LEM}$ at line 2. There the goal is a disjunction neither of whose sides holds for every balanced $n$ (at $n = 7$ the left fails, at $n = 6$ the right): the case “When $\mathrm{RAA}$ earns its place” names.

Exercise (R3)

Let $n$ be an integer, $P$ : “ $n$ is a multiple of $6$ ”, $Q$ : “ $n$ is even”, so that $P \to Q$ is true. For each statement, say whether it follows from $P \to Q$ by the rules so far, naming the result that gives it, or break the step from $P \to Q$ to it at a value of $n$ : (i) $\neg Q \to \neg P$ ; (ii) $Q \to P$ ; (iii) $\neg P \to \neg Q$ ; (iv) $\neg P \vee Q$ ; (v) $P \to (P \wedge Q)$ ; (vi) $P \leftrightarrow Q$ . Which of the derivations you cite uses a classical line ( $\mathrm{RAA}$ , $\mathrm{\neg\neg E}$ or $\mathrm{LEM}$ )?

Solution.

(i) Follows: Proposition 2.3.2 ( $\mathrm{CP}$ ).
(ii) Breaks at $n = 2$ : $P \to Q$ is true, $Q$ is true and $P$ false, so $Q \to P$ is false.
(iii) Breaks at $n = 2$ : $\neg P$ is true and $\neg Q$ false.
(iv) Follows: Proposition 2.5.6, the direction $P \to Q \vdash \neg P \vee Q$ , whose derivation in this section uses $\mathrm{LEM}$ . It is the one cited derivation with a classical line.
(v) Follows, with no classical line:

1 $P \to Q$
2 $P$ asm, for $\mathrm{{{\to}}I}$
3 $Q$ $\mathrm{{{\to}}E}$ 1, 2
4 $P \wedge Q$ $\mathrm{{\wedge}I}$ 2, 3
5 $P \to (P \wedge Q)$ $\mathrm{{{\to}}I}$ 2–4
(vi) Breaks at $n = 2$ : $P$ is false and $Q$ true.

The breaks are of the step with this $P$ and $Q$ : at $n = 2$ the premise is true (a multiple of $6$ is $6k = 2(3k)$ , so $P \to Q$ holds for every $n$ ) and the conclusion false, so the form is bad.