3.1 How to Find a Derivation

We now have every rule for the connectives. Checking a derivation is mechanical, as Definition 1.4.2 makes it: for each line, which rule, which lines, and are they available. Finding one is not, since an assumption may be any statement at all. Yet every Idea in Chapters 1 and 2 found its derivation with the same handful of moves. This section introduces no new rule. It collects those moves into one method, puts them in order, says why the order is right, and then watches the method work: on five searches that succeed, one that fails, and one mathematical goal. It ends with every rule in one place.

3.1.1. The moves so far

Each section since Section 1.2 has added a move, either to the list read off the goal (goal-directed: which introduction rule builds the goal’s main connective?) or to the list read off the premises (premise-directed: which elimination rule uses an available line’s main connective?). Here they are together, with the section where each first appeared.

The situation	The move	First met
goal $\varphi \wedge \psi$	two subgoals, $\varphi$ and $\psi$ , joined by $\mathrm{\wedge I}$	Section 1.2
resource $\varphi \wedge \psi$	take it apart by $\mathrm{\wedge E}$	Section 1.2
resource $\varphi \to \psi$	fire it on $\varphi$ by $\mathrm{{\to}E}$ ; if $\varphi$ is missing, make it a subgoal	Section 1.3
goal $\varphi \to \psi$	a box opened with $\varphi$ , with the new goal $\psi$	Section 1.4
goal $\varphi \vee \psi$	postpone; choose a side only when it is in hand	Section 1.5
resource $\varphi \vee \psi$	two cases, each ending in the current goal	Section 1.6
goal $\bot$	find a clash, or manufacture one; an impossible case closes itself by $\mathrm{\bot E}$	Section 2.1
resource $\neg\varphi$	clash it by $\mathrm{\neg E}$ : make $\varphi$ a subgoal	Section 2.1
goal $\neg\varphi$	a box opened with $\varphi$ , with the new goal $\bot$	Section 2.2
a pattern with a name	use the derived rule as one line ( $\mathrm{MT}$ , $\mathrm{DS}$ , …)	Section 2.3
goal $\varphi \leftrightarrow \psi$	two boxes, one for each direction	Section 2.4
resource $\varphi \leftrightarrow \psi$	cross it by $\mathrm{{\leftrightarrow}E}$ once one side is on a line	Section 2.4
stuck	assume the negation of the goal ( $\mathrm{RAA}$ ), or split on $\chi \vee \neg\chi$ ( $\mathrm{LEM}$ )	Section 2.5

Thirteen moves is a lot to hold in mind at a blank page. The method below turns them into an order of attack. Every assumption a search opens says, in its justification column, which move opened it: “asm, for $\mathrm{{\to}I}$ ” is the goal step for $\to$ , “asm, for $\mathrm{\vee E}$ ” the resource step for $\vee$ , “asm, for $\mathrm{RAA}$ ” step 5. To state it we need a name for a derivation that is only half written.

3.1.2. Partial derivations

Here is the first snapshot of the first search below, for $P \to \neg Q \vdash \neg(P \wedge Q) \wedge (Q \to \neg P)$ , drawn as in every section since Section 1.2:

P \to \neg Q

\vdots

\neg (P \wedge Q)

\vdots

Q \to \neg P

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

\mathrm{{\wedge}I}

7, 13

Each row $\vdots$ is a gap. The written line just below a gap, here line 7 or line 13, is the gap’s current goal; it has no justification yet. The lines available at that goal, here the premise for the first gap and the premise and line 7 for the second, are the gap’s resources. The definition says the same thing exactly.

Definition 3.1.1 (Partial Derivation)

A partial derivation is a list of lines laid out as a derivation (Definition 1.4.2), except that some stretches of lines are still missing. Each missing stretch is a gap, drawn as a row $\vdots$ . The line just below a gap is its current goal; it is already written, but it has no justification yet, since the lines of the gap are to supply one. The lines available at the current goal, in the sense of Definition 1.4.2, are the gap’s resources.

In words: every line that has been written is a premise, an assumption, a current goal, or a line justified by a rule from lines and boxes available to it; the boxes are nested and closed as in any derivation; only the gaps are missing. A search starts with a single gap, below the premises and above the conclusion, and each step replaces a gap by lines, boxes, and smaller gaps. It ends when no gap is left, and then the partial derivation is a derivation.

The snapshots in the worked searches below are all partial derivations; a line carries the number it will have in the finished derivation, and a line whose place is not yet fixed carries no number. On paper you would number the lines at the end.

Second readingA snapshot that is not a partial derivation

Nonexample. Take a snapshot and leave one of its boxes open at the bottom, so that the conclusion sits inside the box. That is not a partial derivation, even though every line is correct so far: Definition 1.4.2 asks that every box close and that the last line lie outside every box, and a gap cannot repair that, since filling a gap adds lines only above its current goal.

3.1.3. The method

Work from both ends: let the goal choose the boxes, let the premises choose the eliminations, and meet in the middle.

Algorithm. Searching for a derivation of $\Gamma \vdash \varphi$ .

Set up. Write the premises $\Gamma$ at the top and $\varphi$ at the bottom, with one gap between.
Goal-directed step. Take the main connective of the current goal (Definition 1.1.2) and set up its introduction rule:
- $\psi \wedge \chi$ : two gaps, with goals $\psi$ and $\chi$ (Section 1.2);
- $\psi \to \chi$ : a box opened with $\psi$ ; inside it, the new goal is $\chi$ (Section 1.4);
- $\neg\psi$ : a box opened with $\psi$ ; inside it, the new goal is $\bot$ (Section 2.2);
- $\psi \leftrightarrow \chi$ : two boxes, one from $\psi$ to $\chi$ and one from $\chi$ to $\psi$ (Section 2.4);
- $\psi \vee \chi$ : postpone; do not choose a side yet (Section 1.5).
Repeat while the current goal is a $\wedge$ , $\to$ , $\neg$ , or $\leftrightarrow$ .
Premise-directed step. Take the main connective of a resource and apply its elimination rule: $\mathrm{\wedge E}$ freely (Section 1.2); $\mathrm{{\to}E}$ and $\mathrm{{\leftrightarrow}E}$ when the other statement they need is a resource, or can be made a new goal (Sections 1.3 and 2.4); $\mathrm{\vee E}$ by opening two boxes, one per disjunct, each ending in the current goal (Section 1.6). A derived rule may do the work of several lines (Section 2.3): a resource $\psi \to \chi$ with $\neg\chi$ available gives $\neg\psi$ by $\mathrm{MT}$ ; a resource $\psi \vee \chi$ with $\neg\psi$ available gives $\chi$ by $\mathrm{DS}$ .
Clash. If the current goal is $\bot$ , look for a pair $\chi$ , $\neg\chi$ among the resources, or make $\chi$ the new goal for some resource $\neg\chi$ and manufacture it, starting again at step 2 for that goal. Whatever the current goal, if the resources clash, or a clash with a resource $\neg\chi$ can be manufactured, write $\bot$ and then the goal by $\mathrm{\bot E}$ : an impossible case closes itself (Section 2.1). When the clash needs a disjunction whose negation is a resource, either side may be chosen to build it: once the disjunction is written, $\bot$ follows.
Stuck. Use $\mathrm{RAA}$ : open a box with the negation of the current goal, whose new goal is $\bot$ ; if that gives nothing, try the same with a goal further out whose box contains the stalled gap. Or use $\mathrm{LEM}$ on a well-chosen statement $\chi$ , and split on $\chi \vee \neg\chi$ by $\mathrm{\vee E}$ . Then return to step 3 (Section 2.5).

When no gap is left, number the lines and check the derivation as Definition 1.4.2 says.

The steps are listed in the order in which to try them, and the order has reasons.

Step 2 loses nothing. If a gap with the goal $\psi \to \chi$ can be filled at all, so can the gap inside a box on $\psi$ with the goal $\chi$ .
Choosing a side of $\vee$ can leave a goal that does not follow. From $P \vee Q$ , with $P$ true and $Q$ false, the step to $Q$ breaks.
Step 5 loses nothing either, and still comes last. The goal $\bot$ gives step 2 nothing to work with, and a good statement to split on must be chosen.

Second readingWhy the order loses nothing

The goal-directed steps lose nothing. Suppose the goal $\psi \to \chi$ is derivable from the resources $\Gamma$ at all, by some derivation $D$ . Then $\chi$ is derivable from $\Gamma$ together with $\psi$ : add $\psi$ to the premises of $D$ (Definition 1.2.3 asks only that the premises belong to the list), and append the line $\chi$ by $\mathrm{{\to}E}$ , citing the last line of $D$ and the premise $\psi$ . A derivation from $\Gamma$ and $\psi$ can be written inside the box, its premises from $\Gamma$ cited as available lines and $\psi$ as the box’s assumption (the pasting of Lemma 2.3.3). So opening a box on $\psi$ never turns a derivable gap into an underivable one. With $\mathrm{\wedge E}$ , $\mathrm{\neg E}$ , or $\mathrm{{\leftrightarrow}E}$ as the appended line, the same argument covers $\wedge$ , $\neg$ , and $\leftrightarrow$ . That is why step 2 may be applied without thinking.

Choosing a side of $\vee$ can leave a goal that does not follow. A disjunction can be derivable when neither side follows from the resources. From $P \vee Q$ the goal $Q \vee P$ is derivable (Example (First derivations with “or”)), but $P \vee Q$ does not say which side holds, so a last line $\mathrm{\vee I}$ from $Q$ , or from $P$ , leaves a gap whose goal does not follow from its resources: $P$ true and $Q$ false makes $P \vee Q$ true and $Q$ false. Choosing a side is safe only once the resources decide it, typically inside a case of $\mathrm{\vee E}$ , or when the disjunction is being manufactured for a clash (step 4) with a resource that is its negation: then the resources derive $\bot$ as soon as they derive the disjunction, and from $\bot$ every statement, either side included, by $\mathrm{\bot E}$ .

Step 5 also loses nothing, and still comes last. If $\varphi$ is derivable from the resources, then $\bot$ is derivable from them together with $\neg\varphi$ , by one appended $\mathrm{\neg E}$ ; so an $\mathrm{RAA}$ box is always safe. A split on $\chi \vee \neg\chi$ is safe too, since each case only adds a resource. Step 5 comes last because the goal $\bot$ gives step 2 nothing to work with, because a good $\chi$ must be chosen, and because a derivation that did not need the classical step reads worse with it (the costume of Section 2.5).

The same method as a chart. A move counts only if the gap it makes is not already open above it, with the same goal and resources. When no move is left, go back to the gap that made this one.

$Diagram. Labels: no, a gap: its goal\and its resources, is the goal\a resource?, is the goal a wedge , to ,\\neg or leftrightarrow ?, can a resource be taken\apart by a move untried\for this gap?, is the goal bot , or do the\resources clash, with a clash\untried for this gap?, is RAA on this goal, or LEM on\a well-chosen statement,\still untried for this gap?, no move left: back to the gap\that made this one; at the first\gap , stop and try to break the claim, done: cite it,\or copy it by R, step 2: its introduction\rule (boxes or two gaps), step 3: its elimination rule\\(veeE : both boxes end in the goal), step 4: find or build\the clash; botE if needed, step 5: RAA on the goal\\(not bot ), or LEM\on that statement$

Quick check. For each goal, with no premises, name the first rule the method aims for and the box or gaps it sets up.

(a) $\neg(P \wedge \neg P)$
(b) $(P \vee Q) \to (Q \vee P)$
(c) $(P \to Q) \wedge (Q \to (P \to Q))$
(d) $P \vee \neg(P \wedge Q)$

Solution.

(a) $\mathrm{\neg I}$ : a box opened with $P \wedge \neg P$ , goal $\bot$ . (b) $\mathrm{{\to}I}$ : a box opened with $P \vee Q$ , goal $Q \vee P$ ; that goal is a disjunction, so it is postponed, and step 3 uses the new resource $P \vee Q$ by $\mathrm{\vee E}$ . (c) $\mathrm{\wedge I}$ : two gaps, with goals $P \to Q$ and $Q \to (P \to Q)$ , each then a box. (d) Step 2 postpones the disjunction, and with no premises steps 3 and 4 have nothing to use, so the search is at step 5 at once. $\mathrm{LEM}$ on $P$ works: in the case $P$ , $\mathrm{\vee I}$ gives the left side; in the case $\neg P$ , a $\mathrm{\neg I}$ box on $P \wedge Q$ clashes (its $\mathrm{\wedge E}$ gives $P$ ) and gives $\neg(P \wedge Q)$ , and $\mathrm{\vee I}$ gives the right side.

3.1.4. Splitting the goal

We now run the method. The first search uses only steps 2, 3, and 4. It is the full version of the chapter’s main move, read the skeleton off the goal, then work from both ends, which comes back twice in the exercises with parts left blank.

Example (Splitting the goal, then using the premise)

Find a derivation of $P \to \neg Q \vdash \neg(P \wedge Q) \wedge (Q \to \neg P)$ .

Solution. Step 1. The premise on top, the goal at the bottom, one gap. The resources of the gap are the premise alone.

Step 2, first pass. The goal’s main connective is $\wedge$ , so it splits into two gaps, with goals $\neg(P \wedge Q)$ and $Q \to \neg P$ , joined at the end by $\mathrm{\wedge I}$ :

P \to \neg Q

\vdots

\neg (P \wedge Q)

\vdots

Q \to \neg P

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

\mathrm{{\wedge}I}

7, 13

Step 2, again. Both new goals have a connective, so step 2 applies to each. The goal $\neg(P \wedge Q)$ asks for a $\mathrm{\neg I}$ box opened with $P \wedge Q$ and ending in $\bot$ . The goal $Q \to \neg P$ asks for a $\mathrm{{\to}I}$ box opened with $Q$ ; inside it the goal $\neg P$ asks, in turn, for a $\mathrm{\neg I}$ box opened with $P$ . Every gap now has the goal $\bot$ , and step 2 has nothing more to do:

P \to \neg Q

P \wedge Q

asm, for

\mathrm{{\neg}I}

\vdots

\bot

\neg (P \wedge Q)

\mathrm{{\neg}I}

2–6

Q

asm, for

\mathrm{{{\to}}I}

P

asm, for

\mathrm{{\neg}I}

\vdots

\bot

\neg P

\mathrm{{\neg}I}

9–11

Q \to \neg P

\mathrm{{{\to}}I}

8–12

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

\mathrm{{\wedge}I}

7, 13

Steps 3 and 4, first gap. The resources are lines 1 and 2. Step 3 splits line 2 into $P$ and $Q$ by $\mathrm{\wedge E}$ . Now $P$ is the hypothesis of line 1, so $\mathrm{{\to}E}$ gives $\neg Q$ . Step 4 finds the pair $Q$ , $\neg Q$ .

Steps 3 and 4, second gap. The resources are lines 1, 7, 8, and 9, and line 7 is not needed.

Givens	Goal
$P \to \neg Q$ , $\neg(P \wedge Q)$ , $Q$ , $P$	$\bot$
… and $\neg Q$ (→E 1, 9)	$\bot$ ✓ ( $Q$ and $\neg Q$ clash)

$\mathrm{{\to}E}$ on lines 1 and 9 gives $\neg Q$ , which clashes with line 8. Both gaps close:

P \to \neg Q

P \wedge Q

asm, for

\mathrm{{\neg}I}

P

\mathrm{{\wedge}E}

Q

\mathrm{{\wedge}E}

\neg Q

\mathrm{{{\to}}E}

1, 3

\bot

\mathrm{{\neg}E}

4, 5

\neg (P \wedge Q)

\mathrm{{\neg}I}

2–6

Q

asm, for

\mathrm{{{\to}}I}

P

asm, for

\mathrm{{\neg}I}

\neg Q

\mathrm{{{\to}}E}

1, 9

\bot

\mathrm{{\neg}E}

8, 10

\neg P

\mathrm{{\neg}I}

9–11

Q \to \neg P

\mathrm{{{\to}}I}

8–12

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

\mathrm{{\wedge}I}

7, 13

What the method did. The goal-directed steps wrote nine of the fourteen lines, every box among them, before the premise was used; the premise-directed steps wrote four, lines 3, 4, 5, and 10. The premise itself was used once in each gap, by the same $\mathrm{{\to}E}$ . Line 10 cites line 1 from inside two boxes, which is legal because line 1 is a premise and so is available everywhere below it.

Notice how little thinking the search needed. That is the typical shape of a successful search: the goal fixes the skeleton, and the premises fill in the flesh.

Quick check. In the second snapshot of Example (Splitting the goal, then using the premise) above, the second gap has the current goal $\bot$ on line 11, and line 7 is one of its resources, though the gap never uses it. Why is line 7 available there, and why are lines 2–6 not?

Solution. Line 7 lies in no box and above the gap, so it is available, though this gap will not need it. Lines 2–6 are not resources: they lie in a box that has closed.

3.1.5. Cases must end in the goal

When the goal gives nothing, the premises must. The next search is driven by a disjunction among the premises.

Example (Proof by cases, found by the method)

Find a derivation of $P \vee Q, \ P \to R, \ Q \to R \vdash R$ .

Solution. Step 1. The premises, one gap, the goal:

P \vee Q

P \to R

Q \to R

\vdots

R

The goal $R$ is a letter, so step 2 has nothing to do. Step 3 looks at the resources. $\mathrm{{\to}E}$ on $P \to R$ needs $P$ , and making $P$ a new goal is hopeless: from $P \vee Q$ we know that one of $P$ , $Q$ holds, not which. The disjunction itself is the resource to use, by $\mathrm{\vee E}$ , with two boxes that each end in the current goal $R$ :

P \vee Q

P \to R

Q \to R

P

asm, for

\mathrm{{\vee}E}

\vdots

R

Q

asm, for

\mathrm{{\vee}E}

\vdots

R

R

\mathrm{{\vee}E}

1, 4–5, 6–7

Inside the first box, $P$ is a resource, so $\mathrm{{\to}E}$ on line 2 closes the gap at once; the second box is the same with line 3:

P \vee Q

P \to R

Q \to R

P

asm, for

\mathrm{{\vee}E}

R

\mathrm{{{\to}}E}

2, 4

Q

asm, for

\mathrm{{\vee}E}

R

\mathrm{{{\to}}E}

3, 6

R

\mathrm{{\vee}E}

1, 4–5, 6–7

This is the pattern that Section 1.6 called the skeleton of almost every proof by cases (compare Example (Cases on a hypothesis are two implications), which packages the same two boxes into one implication). The method found it without being told.

Why the boxes end in the current goal. $\mathrm{\vee E}$ (Definition 1.6.1) gives, after the two boxes, their common last line and nothing else. A box that ends in anything but the current goal leaves that goal still to be reached, and two boxes that end in different statements cannot be combined at all.

3.1.6. Postponing a disjunction

The third search has a disjunction as its goal. It shows why step 2 postpones one, and how a dead end can name the statement to split on.

Example (Choosing a side too early)

Find a derivation of $P \to (Q \vee R) \vdash (P \to Q) \vee (P \to R)$ .

Solution. The tempting start. The goal is a disjunction, and it is tempting to choose a side at once, say $P \to Q$ , and finish with $\mathrm{\vee I}$ . The new goal is an implication, so we open a box on $P$ ; then $\mathrm{{\to}E}$ gives $Q \vee R$ , and $\mathrm{\vee E}$ splits into the cases $Q$ and $R$ , each to end in the current goal $Q$ . The first case ends at once. The second is a dead end:

P \to (Q \vee R)

P

asm, for

\mathrm{{{\to}}I}

Q \vee R

\mathrm{{{\to}}E}

1, 2

Q

asm, for

\mathrm{{\vee}E}

R

asm, for

\mathrm{{\vee}E}

\vdots

Q

Q

\mathrm{{\vee}E}

P \to Q

\mathrm{{{\to}}I}

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

\mathrm{{\vee}I}

In the case $R$ the resources are $P \to (Q \vee R)$ , $P$ , $Q \vee R$ , and $R$ , and none of them yields $Q$ : no resource has $Q$ as a conclusion except $Q \vee R$ , which is already split, and nothing clashes. Choosing the right side instead fails in the mirror image, in the case $Q$ . In fact neither side follows from the premise alone: with $P$ and $Q$ true and $R$ false the premise is true and $P \to R$ is false, and with $P$ and $R$ true and $Q$ false the premise is true and $P \to Q$ is false.

The diagnosis. Each case of the dead end knew which side it wanted: the case $Q$ wanted $P \to Q$ , and the case $R$ wanted $P \to R$ . But those cases were opened inside the box of $P$ , too late to choose the side of a disjunction that stands outside it. The side must be decided before any box is opened, and the premise does not decide it. Steps 2–4 are used up: we are at step 5.

The dead end also names the statement to split on. If $Q$ holds, the left side is easy. If $Q$ fails, then from $P$ the premise gives $Q \vee R$ with its left side refuted, and $\mathrm{DS}$ gives $R$ . So we use $\mathrm{LEM}$ on $Q$ , and each case gets the whole goal:

P \to (Q \vee R)

Q \vee \neg Q

\mathrm{LEM}

Q

asm, for

\mathrm{{\vee}E}

\vdots

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

\neg Q

asm, for

\mathrm{{\vee}E}

\vdots

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

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

\mathrm{{\vee}E}

2, 3–7, 8–13

Now each case decides the side. In the case $Q$ , the goal is $P \to Q$ : a box on $P$ whose last line repeats $Q$ . In the case $\neg Q$ , the goal is $P \to R$ : a box on $P$ , then $Q \vee R$ by $\mathrm{{\to}E}$ , then $R$ by Proposition 2.3.4 used as a derived rule, citing $Q \vee R$ and $\neg Q$ . Then $\mathrm{\vee I}$ , on the correct side each time:

P \to (Q \vee R)

Q \vee \neg Q

\mathrm{LEM}

Q

asm, for

\mathrm{{\vee}E}

P

asm, for

\mathrm{{{\to}}I}

Q

\mathrm{R}

P \to Q

\mathrm{{{\to}}I}

4–5

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

\mathrm{{\vee}I}

\neg Q

asm, for

\mathrm{{\vee}E}

P

asm, for

\mathrm{{{\to}}I}

Q \vee R

\mathrm{{{\to}}E}

1, 9

R

\mathrm{DS}

10, 8

P \to R

\mathrm{{{\to}}I}

9–11

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

\mathrm{{\vee}I}

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

\mathrm{{\vee}E}

2, 3–7, 8–13

What the method did. Step 2 postponed the goal, the tempting start broke that rule, and its dead end showed both why the rule exists and what to do instead. Line 5 repeats line 3 because $\mathrm{{\to}I}$ needs $Q$ as a line of the box of line 4 itself.

Warning. Do not choose a disjunct early. A goal $\psi \vee \chi$ tempts us to pick a side and prove it, and the choice usually fails, as the first attempt above did: neither $P \to Q$ nor $P \to R$ follows from the premise. Postpone the $\vee$ goal, use the resources first, and choose a side only inside a case that decides it.

3.1.7. When nothing else works

The fourth search reaches step 5 in the other form, $\mathrm{RAA}$ , and then needs steps 2 and 4 inside the box.

Example (A search that reaches step 5 at once)

Find a derivation of $\neg(P \leftrightarrow Q) \vdash P \vee Q$ .

Solution. Steps 1–4. The goal is a disjunction, so step 2 postpones it. The one resource is a negation, and a negation can be used only in a clash (step 4), and here no clash can be found or manufactured. Neither side is in hand: the premise says only that $P$ and $Q$ differ, not which one holds. Steps 2–4 have nothing to offer.

Step 5. We assume the negation of the goal. The new goal is $\bot$ , and the gap has one more resource:

\neg (P \leftrightarrow Q)

\neg (P \vee Q)

asm, for

\mathrm{RAA}

\vdots

\bot

P \vee Q

\mathrm{RAA}

2–12

Step 4 inside the box. The resources are two negations, $\neg(P \leftrightarrow Q)$ and $\neg(P \vee Q)$ , and no pair clashes yet. So we choose a statement to manufacture: $P \leftrightarrow Q$ , to clash with line 1, or $P \vee Q$ , to clash with line 2. The second is the goal we started from, a disjunction of two letters with no side in hand, so aiming at it leads back to the start. So we choose $P \leftrightarrow Q$ , and it is a biconditional, so step 2 sets up two boxes:

\neg (P \leftrightarrow Q)

\neg (P \vee Q)

asm, for

\mathrm{RAA}

P

asm, for

\mathrm{{{\leftrightarrow}}I}

\vdots

Q

Q

asm, for

\mathrm{{{\leftrightarrow}}I}

\vdots

P

P \leftrightarrow Q

\mathrm{{{\leftrightarrow}}I}

3–6, 7–10

\bot

\mathrm{{\neg}E}

11, 1

P \vee Q

\mathrm{RAA}

2–12

The two small gaps. In the first, the resources are lines 1, 2, and 3, and the goal $Q$ is a letter that no resource produces. But the resources clash once a line is manufactured: $\mathrm{\vee I}$ builds $P \vee Q$ from line 3, which clashes with line 2, and $\mathrm{\bot E}$ writes $Q$ (step 4: an impossible case closes itself). The second gap is the mirror image:

\neg (P \leftrightarrow Q)

\neg (P \vee Q)

asm, for

\mathrm{RAA}

P

asm, for

\mathrm{{{\leftrightarrow}}I}

P \vee Q

\mathrm{{\vee}I}

\bot

\mathrm{{\neg}E}

4, 2

Q

\mathrm{{\bot}E}

Q

asm, for

\mathrm{{{\leftrightarrow}}I}

P \vee Q

\mathrm{{\vee}I}

\bot

\mathrm{{\neg}E}

8, 2

P

\mathrm{{\bot}E}

P \leftrightarrow Q

\mathrm{{{\leftrightarrow}}I}

3–6, 7–10

\bot

\mathrm{{\neg}E}

11, 1

P \vee Q

\mathrm{RAA}

2–12

What the method did. Step 5 came first, because nothing else applied, and after it steps 2 and 4 did the rest: step 4 chose which clash to aim for, step 2 read the two boxes off $P \leftrightarrow Q$ , and step 4 closed each box with a manufactured clash and $\mathrm{\bot E}$ . In words: suppose neither $P$ nor $Q$ holds; then each of them implies the other, since neither can hold at all; so $P \leftrightarrow Q$ , against the premise. The assumption of line 2 is used twice, at lines 5 and 9.

Second readingOther splits that also work

In Example (Choosing a side too early). $\mathrm{LEM}$ on $P$ , the first split one thinks of, also succeeds, but less well: in the case $P$ the premise gives $Q \vee R$ , and a second $\mathrm{\vee E}$ , with two more implication boxes, is needed inside it; the finished derivation has 22 lines against these 14.

In Example (A search that reaches step 5 at once). A split by $\mathrm{LEM}$ on $P$ also works, but less well: in the case $\neg P$ the goal side $Q$ is a letter that the resources do not give, and the search is stuck there a second time.

Step 5’s advice to try a goal further out is shown on Peirce’s law in the fold below.

Second readingStep 5 one level out: the search for Peirce’s law

The derivation of Peirce’s law (Proposition 2.5.4, in the fold of Section 2.5) adds one detail to step 5.

(P \to Q) \to P

asm, for

\mathrm{{{\to}}I}

P

asm, for

\mathrm{{{\to}}I}

\vdots

Q

P \to Q

\mathrm{{{\to}}I}

P

\mathrm{{{\to}}E}

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

\mathrm{{{\to}}I}

In the box on $P$ with the goal $Q$ , the search stalls: assuming $\neg Q$ gives nothing new, since a clash with $\neg Q$ needs $Q$ itself. One level out, the search assumes $\neg P$ :

(P \to Q) \to P

asm, for

\mathrm{{{\to}}I}

\neg P

asm, for

\mathrm{RAA}

P

asm, for

\mathrm{{{\to}}I}

\vdots

Q

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 new resource $\neg P$ is available in every gap inside its box, including the stalled one, where it clashes with line 3. That is why step 5 says to try a goal further out.

Quick check. In the second snapshot, which two resources of the gap clash, and what does $\mathrm{\bot E}$ then write?

Solution. Lines 3 ( $P$ ) and 2 ( $\neg P$ ) give $\bot$ by $\mathrm{\neg E}$ 3, 2 at line 4, and $\mathrm{\bot E}$ 4 writes $Q$ , line 5.

The method finds a derivation; these four refinements usually find a shorter or more direct one.

Find the goal among the resources. Before step 2, ask whether the current goal is already available; if so, cite it, or copy it into the current box by $\mathrm{R}$ .
Derive what needs nothing new before opening a box. $\mathrm{\wedge E}$ on a resource, and $\mathrm{{\to}E}$ or $\mathrm{{\leftrightarrow}E}$ when both of their lines stand, may be written at once, above the boxes the goal asks for: a line outside the boxes is available inside all of them, so it is written once instead of once per box. ( $\mathrm{\vee E}$ is not such a step: it opens boxes.)
Look first for a clash partner already on a line. When the goal is $\bot$ , scan the resources for a negation $\neg\chi$ whose $\chi$ is cheap, or for $\chi$ and $\neg\chi$ both in reach, before manufacturing anything (step 4).

Example (Lines that need nothing new)

Find a derivation of $P \wedge (P \to Q), \ Q \to R \vdash (S \to R) \wedge (T \to (Q \wedge R))$ .

Solution. The search. The goal is a conjunction of two implications, so step 2 will open a box on $S$ and a box on $T$ :

P \wedge (P \to Q)

Q \to R

\vdots

(S \to R) \wedge (T \to (Q \wedge R))

Before it does, the resources give lines that need nothing new: $P$ and $P \to Q$ by $\mathrm{\wedge E}$ , then $Q$ by $\mathrm{{\to}E}$ , and then $R$ by $\mathrm{{\to}E}$ on the second premise. With $Q$ and $R$ outside every box, the two boxes are short:

P \wedge (P \to Q)

Q \to R

P

\mathrm{{\wedge}E}

P \to Q

\mathrm{{\wedge}E}

Q

\mathrm{{{\to}}E}

4, 3

R

\mathrm{{{\to}}E}

2, 5

S

asm, for

\mathrm{{{\to}}I}

\vdots

R

S \to R

\mathrm{{{\to}}I}

7–8

T

asm, for

\mathrm{{{\to}}I}

\vdots

Q \wedge R

T \to (Q \wedge R)

\mathrm{{{\to}}I}

10–11

(S \to R) \wedge (T \to (Q \wedge R))

\mathrm{{\wedge}I}

9, 12

In the box of $S$ the goal $R$ is a resource, copied by $\mathrm{R}$ . In the box of $T$ , $\mathrm{\wedge I}$ joins $Q$ and $R$ :

P \wedge (P \to Q)

Q \to R

P

\mathrm{{\wedge}E}

P \to Q

\mathrm{{\wedge}E}

Q

\mathrm{{{\to}}E}

4, 3

R

\mathrm{{{\to}}E}

2, 5

S

asm, for

\mathrm{{{\to}}I}

R

\mathrm{R}

S \to R

\mathrm{{{\to}}I}

7–8

T

asm, for

\mathrm{{{\to}}I}

Q \wedge R

\mathrm{{\wedge}I}

5, 6

T \to (Q \wedge R)

\mathrm{{{\to}}I}

10–11

(S \to R) \wedge (T \to (Q \wedge R))

\mathrm{{\wedge}I}

9, 12

Quick check. In Example (Lines that need nothing new), which refinement does line 8 use, and which do lines 3–6 use?

Solution. Line 8 finds the goal $R$ among the resources (line 6) and copies it into the box of $S$ . Lines 3–6 need nothing new and are written before any box opens, so both boxes can use them.

No detours. Never build a line by an introduction rule and then, at once, take that line apart by the matching elimination. The line the pair produces was within reach without it. This includes $\mathrm{\neg I}$ followed by $\mathrm{\neg E}$ on the negation it built. A manufactured clash is not a detour: $\mathrm{\vee I}$ followed by $\mathrm{\neg E}$ against $\neg(\varphi \vee \psi)$ uses the new line with a different connective. The book uses this as advice, not as a theorem: a detour is legal, and cutting one need not shorten a derivation, since an introduced line cited elsewhere stays.

Second readingWhy a detour’s line was within reach

After $\mathrm{\wedge I}$ joins lines $i$ and $j$ , $\mathrm{\wedge E}$ on the new line gives back line $i$ or line $j$ . After $\mathrm{{\to}I}$ closes a box from $\varphi$ to $\psi$ , $\mathrm{{\to}E}$ on the new implication and a line $\varphi$ gives $\psi$ ; the box’s lines, copied with that line in place of the assumption, give $\psi$ directly. After $\mathrm{\neg I}$ closes a box from $\varphi$ to $\bot$ , $\mathrm{\neg E}$ on the new negation and a line $\varphi$ gives $\bot$ ; the box’s lines, copied likewise, give $\bot$ directly. After $\mathrm{\vee I}$ builds $\varphi \vee \psi$ from a line $\varphi$ , $\mathrm{\vee E}$ on it gives what its first case gives, and the first case’s lines, copied with the line $\varphi$ in place of the assumption, give that directly. Every copied citation stays legal by the scope rule of Definition 1.4.2, since the line put in place of the assumption stands above the copy.

Quick check. Lines 2 and 3 are $P$ and $R$ ; line 4 is $P \wedge R$ , $\mathrm{\wedge I}$ 2, 3; line 5 is $R$ , $\mathrm{\wedge E}$ 4. Which refinement does this break, and what should line 5 cite instead?

Solution. No detours. Lines 4–5 build a conjunction and take it apart at once; line 5’s statement is line 3, so cite line 3, or copy it by $\mathrm{R}$ where it must lie in the current box.

3.1.9. A search that fails

The method is not a machine that always succeeds. Here it fails, and the failure is instructive.

Try $P \to Q \vdash Q \to P$ . Step 2 opens a box on $Q$ with the goal $P$ :

P \to Q

Q

asm, for

\mathrm{{{\to}}I}

\vdots

P

Q \to P

\mathrm{{{\to}}I}

Every further move goes round in a circle:

Attempt	What it needs	Why that goes round in a circle
step 3: $\mathrm{{\to}E}$ on line 1	$P$	$P$ is the goal
step 4: a clash	a negation among the resources	there is none
step 5: $\mathrm{RAA}$ , a box on $\neg P$	$P$ , to clash with $\neg P$	$P$ is the goal
step 5: $\mathrm{LEM}$ on $P$	in the case $\neg P$ , the goal $P$	the same gap, one resource richer and no closer
step 5 further out: $\mathrm{RAA}$ on $\neg(Q \to P)$	$Q \to P$ , to clash	step 2 opens the same box on $Q$ with the same goal $P$

Every row returns to one gap, “ $P$ from $P \to Q$ and $Q$ ”. That is affirming the consequent (Section 1.3).

Quick check. Which row of the table would close the gap if affirming the consequent were a rule?

Solution. The first: the mirror image of $\mathrm{{\to}E}$ would give $P$ from $P \to Q$ and the resource $Q$ .

But notice what we have not shown. A search that fails proves nothing about derivations in general. An assumption may be any statement at all, by the assumption clause of Definition 1.4.2, so there are infinitely many derivations to consider, and a cleverer one might exist. To show that no derivation of $Q \to P$ from $P \to Q$ exists, we need a different tool.

We show that something is derivable by exhibiting a derivation; how could we ever show that something is not? Section 1.1’s move already breaks Argument B’s form, from $P \to Q$ to $Q \to P$ : with $P$ false and $Q$ true, the premise is true and the conclusion false. What it cannot yet tell us is that no derivation leads from a premise to a conclusion that some choice of statements makes false. Section 3.2 gives this question a sharper form, and the chapter ends on it.

3.1.10. A mathematical goal

The method reads the frame of a proof off the goal whether the statements are letters or facts about numbers. In ordinary mathematics its payoff is that the first and last sentences of a proof, and its division into parts, are fixed before any mathematics is done.

Example (Building a skeleton)

Let $m$ and $n$ be integers. Prove that if $mn$ is odd, then $m$ is odd and $n$ is odd.

Solution. The skeleton. The main connective is “if … then”, so step 2 opens a $\mathrm{{\to}I}$ box: “Assume $mn$ is odd. … Hence $m$ is odd and $n$ is odd.” The new goal is a conjunction, so step 2 again: two separate proofs, one that $m$ is odd and one that $n$ is odd. Each is a letter as far as logic can see, and the one resource, “ $mn$ is odd”, cannot be taken apart. So step 3 brings in facts we can compute with: “if $m$ is even then $mn$ is even” is one, and $\mathrm{CP}$ (Proposition 2.3.2) turns it into “if $mn$ is not even then $m$ is not even”, which the resource can feed. Then “every integer is even or odd” and $\mathrm{DS}$ finish. The givens and the goal are tabulated in the fold below.

The proof. Assume $mn$ is odd. We show that $m$ is odd and that $n$ is odd.

First, if $m$ is even, say $m = 2k$ with $k$ an integer, then $mn = 2(kn)$ is even. By the contrapositive (Proposition 2.3.2), if $mn$ is not even, then $m$ is not even. Now $mn$ is odd, so it is not even, since no integer is both; hence $m$ is not even. Since every integer is even or odd, $m$ is odd, by Proposition 2.3.4.

Exchanging the roles of $m$ and $n$ in the previous paragraph shows that $n$ is odd. Hence $m$ and $n$ are both odd.

What the method did. It fixed the first sentence, the two paragraphs, and the last sentence; the only computation is $mn = 2(kn)$ . No step uses $\mathrm{RAA}$ : the classical-looking move from “ $m$ is not even” to “ $m$ is odd” is disjunctive syllogism on the fact that every integer is even or odd.

Second readingThe givens and the goal

Givens	Goal
the facts: every integer is even or odd, and not both; if $m$ is even, then $mn$ is even; if $n$ is even, then $mn$ is even	if $mn$ is odd, then $m$ is odd and $n$ is odd
… and $mn$ odd (→I)	$m$ odd and $n$ odd
the same	$m$ odd; $n$ odd (∧I: two goals)
… and $mn$ not even (“not both”); $m$ not even (CP, →E)	$m$ odd ✓ (DS); $n$ odd by the same steps, with $m$ and $n$ exchanged

Warning. Do not assume what you want to prove. To derive a goal $\varphi$ , it is tempting to open a box with $\varphi$ . The box reaches $\varphi$ at once, but after it closes it gives $\varphi \to \varphi$ , not $\varphi$ , and its assumption is gone. An assumption is useful when the goal asks for it: the hypothesis of an implication (step 2), the negated goal of $\mathrm{RAA}$ (step 5), a disjunct of a resource (step 3). Opening the box on the conclusion of an implication is the converse error of Argument B, diagnosed in Section 1.4.

Second readingLogic permits; it does not choose

A derivation of $\Gamma \vdash \varphi$ says that whoever accepts every member of $\Gamma$ is committed to $\varphi$ . It does not say that $\varphi$ should now be believed. If $\varphi$ is plainly false, say $0 = 1$ , the derivation is a reason to give up a member of $\Gamma$ , and it does not say which. A mathematician who derives $0 = 1$ from the hypotheses of a lemma has learned that those hypotheses cannot hold together; Section 3.2 calls such a list inconsistent, and a proof by contradiction is built to reach exactly that.

In the other direction, at every gap the rules permit far more lines than any search writes: $\mathrm{\wedge E}$ on every conjunction, $\mathrm{\vee I}$ with any statement at all. The rules choose none of them. The method chooses, and the method is advice, not logic: two searchers may find two different derivations, and both are correct.

3.1.11. The rules in one place

Here are all the primitive rules of Chapters 1 and 2 on one card.

Rule	Shape	You write	Lean
$\mathrm{\wedge I}$	$\varphi$ , $\psi$ $\Longrightarrow$ $\varphi \wedge \psi$	“We show $P$ , and we show $Q$ .”	`constructor`
$\mathrm{\wedge E}$	$\varphi \wedge \psi$ $\Longrightarrow$ $\varphi$ (or $\psi$ )	“In particular, $P$ .”	`h.1` (and `h.2`)
$\mathrm{{\to}E}$	$\varphi \to \psi$ , $\varphi$ $\Longrightarrow$ $\psi$	“Since $P$ implies $Q$ , and $P$ holds, $Q$ .”	`exact h hp`
$\mathrm{{\to}I}$	box $\varphi$ … $\psi$ $\Longrightarrow$ $\varphi \to \psi$	“Assume $P$ . … Hence $Q$ .”	`intro hp`
$\mathrm{R}$	$\varphi$ (available) $\Longrightarrow$ $\varphi$ , copied	“As shown above, $P$ .”	`exact hp`
$\mathrm{\vee I}$	$\varphi$ $\Longrightarrow$ $\varphi \vee \psi$ (or $\psi \vee \varphi$ )	“So $P$ or $Q$ holds.”	`left` (or `Or.inl hp`); `right`
$\mathrm{\vee E}$	$\varphi \vee \psi$ , box $\varphi$ … $\chi$ , box $\psi$ … $\chi$ $\Longrightarrow$ $\chi$	“Case 1: $P$ . … so $R$ . Case 2: $Q$ . … so $R$ . In either case, $R$ .”	`Or.elim h` (or `cases h`)
$\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{{\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`

This is the reference sheet for Chapters 1 and 2: every primitive rule as its schema, with the label that defines it. As in every schema (Definition 1.2.1), $\varphi, \psi, \chi$ stand for any statements, replaced consistently, and $i, j, k, \dots$ for line numbers. Each box rule needs the box’s last line as a line of that box itself, not inside a further box, and every cited line or box must be available (Definition 1.4.2).

Conjunction (Definition 1.2.5): $\mathrm{\wedge I}$ , and the two forms of $\mathrm{\wedge E}$ .

i

\varphi

j

\psi

k

\varphi \wedge \psi

\mathrm{{\wedge}I}

i

j

i

\varphi \wedge \psi

k

\varphi

\mathrm{{\wedge}E}

i

i

\varphi \wedge \psi

k

\psi

\mathrm{{\wedge}E}

i

Implication (Definition 1.4.1): $\mathrm{{\to}I}$ and $\mathrm{{\to}E}$ .

i

\varphi

asm, for

\mathrm{{{\to}}I}

\vdots

j

\psi

k

\varphi \to \psi

\mathrm{{{\to}}I}

i

–

j

i

\varphi \to \psi

j

\varphi

k

\psi

\mathrm{{{\to}}E}

i

j

Disjunction (Definition 1.6.1): the two forms of $\mathrm{\vee I}$ , and $\mathrm{\vee E}$ , whose two boxes end in the same statement $\chi$ .

i

\varphi

k

\varphi \vee \psi

\mathrm{{\vee}I}

i

i

\varphi

k

\psi \vee \varphi

\mathrm{{\vee}I}

i

i

\varphi \vee \psi

j

\varphi

asm, for

\mathrm{{\vee}E}

\vdots

k

\chi

l

\psi

asm, for

\mathrm{{\vee}E}

\vdots

m

\chi

n

\chi

\mathrm{{\vee}E}

i

j

–

k

l

–

m

Contradiction and negation (Definition 2.1.1, Definition 2.2.1): $\mathrm{\neg E}$ , $\mathrm{\bot E}$ (which may write any statement $\varphi$ ), and $\mathrm{\neg I}$ .

i

\varphi

j

\neg \varphi

k

\bot

\mathrm{{\neg}E}

i

j

i

\bot

k

\varphi

\mathrm{{\bot}E}

i

i

\varphi

asm, for

\mathrm{{\neg}I}

\vdots

j

\bot

k

\neg \varphi

\mathrm{{\neg}I}

i

–

j

Biconditional (Definition 2.4.1): $\mathrm{{\leftrightarrow}I}$ , and $\mathrm{{\leftrightarrow}E}$ , which works in both directions.

i

\varphi

asm, for

\mathrm{{{\leftrightarrow}}I}

\vdots

j

\psi

k

\psi

asm, for

\mathrm{{{\leftrightarrow}}I}

\vdots

l

\varphi

m

\varphi \leftrightarrow \psi

\mathrm{{{\leftrightarrow}}I}

i

–

j

k

–

l

i

\varphi \leftrightarrow \psi

j

\varphi

k

\psi

\mathrm{{{\leftrightarrow}}E}

i

j

i

\varphi \leftrightarrow \psi

j

\psi

k

\varphi

\mathrm{{{\leftrightarrow}}E}

i

j

Reductio ad absurdum (Definition 2.5.1), the one classical rule, and repetition, clause (D3) of Definition 1.4.2, which copies an available line into the current box.

i

\neg \varphi

asm, for

\mathrm{RAA}

\vdots

j

\bot

k

\varphi

\mathrm{RAA}

i

–

j

i

\varphi

\vdots

k

\varphi

\mathrm{R}

i

Derived rules. Each is a proved sequent, used as one line that cites the lines holding its premises (Definition 2.3.1). The table lists the sequents of Chapters 1 and 2 that searches use most; every other sequent proved there may be used in the same way. Where a rule has no short name, the justification names the result, as “(ex falso)” or “VI”.

In a justification	Sequent	Proved in	Our derivation uses $\mathrm{RAA}$
(and commutes)	$P \wedge Q \vdash Q \wedge P$	Proposition 1.2.1	no
(implication is transitive)	$P \to Q, \ Q \to R \vdash P \to R$	Proposition 1.4.1	no
(curry)	$(P \wedge Q) \to R \dashv\vdash P \to (Q \to R)$	Proposition 1.4.2	no
(or commutes)	$P \vee Q \vdash Q \vee P$	Example (First derivations with “or”)	no
(or merges)	$P \vee P \vdash P$	Example (First derivations with “or”)	no
(and regroups)	$(P \wedge Q) \wedge R \vdash P \wedge (Q \wedge R)$	Proposition 1.2.2	no
(or regroups)	$P \vee (Q \vee R) \vdash (P \vee Q) \vee R$	Example (Regrouping a disjunction)	no
(distributivity)	$P \wedge (Q \vee R) \dashv\vdash (P \wedge Q) \vee (P \wedge R)$	Proposition 1.6.1	no
(cases on a hypothesis)	$(P \to R) \wedge (Q \to R) \dashv\vdash (P \vee Q) \to R$	Example (Cases on a hypothesis are two implications); the converse Example (A disjunctive hypothesis splits into two implications)	no
$\mathrm{CD}$ (constructive dilemma)	$(P \to R) \wedge (Q \to S), \ P \vee Q \vdash R \vee S$	Example (Constructive dilemma)	no
(destructive dilemma)	$(P \to R) \wedge (Q \to S), \ \neg R \vee \neg S \vdash \neg P \vee \neg Q$	Exercise (B4: Dilemmas as derived rules, used later) (b)	no
(modus ponendo tollens)	$\neg(P \wedge Q) \vdash P \to \neg Q$	Exercise (B4: Dilemmas as derived rules, used later) (c)	no
(ex falso)	$P, \ \neg P \vdash Q$	Proposition 2.1.1	no
VI (vacuous implication)	$\neg P \vdash P \to Q$	Proposition 2.1.2	no
$\mathrm{MT}$	$P \to Q, \ \neg Q \vdash \neg P$	Proposition 2.3.1	no
$\mathrm{CP}$	$P \to Q \vdash \neg Q \to \neg P$	Proposition 2.3.2	no
$\mathrm{DS}$	$P \vee Q, \ \neg P \vdash Q$	Proposition 2.3.4	no
( $\mathrm{DS}$ , other disjunct)	$P \vee Q, \ \neg Q \vdash P$	Exercise (B1: The other disjunctive syllogism, used later) (a)	no
(iff symmetric)	$P \leftrightarrow Q \vdash Q \leftrightarrow P$	Example (An iff read both ways)	no
(iff as two implications)	$P \leftrightarrow Q \dashv\vdash (P \to Q) \wedge (Q \to P)$	Proposition 2.4.1	no
(iff of negations)	$P \leftrightarrow Q \vdash \neg P \leftrightarrow \neg Q$ , and its converse	Example (Negating both sides of an iff); the converse Exercise (B2: Back from negated sides, used later)	the converse only
(equivalence cycle)	$P \to Q, \ Q \to R, \ R \to P \vdash P \leftrightarrow Q$	Proposition 2.4.6	no
$\mathrm{\neg\neg I}$	$P \vdash \neg\neg P$	Proposition 2.5.1 (a), first in Example (Two negations from one premise)	no
$\mathrm{\neg\neg E}$	$\neg\neg P \vdash P$	Proposition 2.5.1 (b)	yes
( $\mathrm{CP}$ , converse)	$\neg Q \to \neg P \vdash P \to Q$	Proposition 2.5.2	yes
$\mathrm{LEM}$	$\vdash P \vee \neg P$	Proposition 2.5.3	yes
(Peirce)	$\vdash ((P \to Q) \to P) \to P$	Proposition 2.5.4	yes
$\mathrm{DM}$	the four laws of Proposition 2.5.5	Proposition 2.5.5	(d) only
(implication as disjunction)	$\neg P \vee Q \vdash P \to Q$ , and its converse	Proposition 2.5.6	the converse only, through $\mathrm{LEM}$

Four rows are proved in exercises, not in the text: the other form of $\mathrm{DS}$ , the destructive dilemma, modus ponendo tollens, and the converse of the iff of negations. Exercises may use them as rules; the text’s own proofs do not.

Each rule is also a move: the table of moves at the start of this section is the decision chart of Section 1.6, grown to every connective, read by the goal for the introduction rules and by an available line for the elimination rules; the chart after the method’s steps draws their order.

Warning. Cite only what is already proved. A derived rule is an abbreviation for its derivation, so it may be used only after that derivation exists, and never inside it. For example, the second route to Proposition 2.5.5 (d) splits on excluded middle; a proof of excluded middle that used De Morgan’s law (d) along that route would be circular. In this book the check is simple: cite only labels that appear earlier.

3.1.12. Exercises

A. Check your understanding

Exercise (A1)

For (a)–(d), name the goal’s main connective, the first rule the method aims for, and the first sentence of a proof. For (e)–(f), name the elimination rule the premise invites, and what it needs.

(a) For real $x$ : if $x^3 < 0$ then $x < 0$ .
(b) There is no integer $n$ with $2n = 7$ .
(c) For real $x$ and $y$ : $\left| xy \right| = \left| x \right|\left| y \right|$ and $\left| x + y \right| \le \left| x \right| + \left| y \right|$ .
(d) For an integer $n$ : $n$ is odd if and only if $n^2$ is odd.
(e) The premise $(P \wedge Q) \to R$ , with the goal $R$ and the resources $P$ and $Q$ .
(f) The premise $\neg(P \vee Q)$ , with the goal $\bot$ and the resource $Q$ .

Solution.

(a) $\to$ ; $\mathrm{{\to}I}$ : “Assume $x^3 < 0$ .” (Starting “Suppose $x \ge 0$ ” inside that frame is an $\mathrm{RAA}$ box on the goal $x < 0$ , not the contrapositive; a proof through the contrapositive replaces the frame, proving “if $x \ge 0$ then $x^3 \ge 0$ ” and then applying $\mathrm{CP}$ .)
(b) $\neg$ , since the claim is “not: there is an integer $n$ with $2n = 7$ ”; $\mathrm{\neg I}$ : “Suppose $n$ is an integer with $2n = 7$ ."
(c) $\wedge$ ; $\mathrm{\wedge I}$ : “We prove the two statements in turn.”
(d) $\leftrightarrow$ ; $\mathrm{{\leftrightarrow}I}$ : “ $(\Rightarrow)$ Assume $n$ is odd.”
(e) $\mathrm{{\to}E}$ , which needs the hypothesis $P \wedge Q$ : make it a new goal, reached by $\mathrm{\wedge I}$ from $P$ and $Q$ ; then $\mathrm{{\to}E}$ gives $R$ .
(f) $\mathrm{\neg E}$ , which needs $P \vee Q$ beside $\neg(P \vee Q)$ : make $P \vee Q$ the new goal (step 4), reached by $\mathrm{\vee I}$ from $Q$ .

Exercise (A2: Drill)

The parts run from one step of the method, through available lines and steps to judge, to short derivations.

(a) The goal is $\neg(P \vee Q)$ . What does step 2 set up?
(b) The goal is $(P \to Q) \wedge \neg R$ . Which gaps does step 2 leave?
(c) The goal is $\bot$ , and the resources are $\neg(P \wedge Q)$ , $P$ , $Q$ . What are the next two lines?
(d) The goal is $P \vee Q$ , and the one resource is $\neg P \to Q$ . Which step does the work, and how?
(e) In a partial derivation the current goal is line 9, inside the boxes opened at lines 3 and 6. Line 1 is a premise, and lines 4–5 form a box inside box 3 that has closed. Which of lines 1, 3, 4, 6 are resources?
(f) Which step of the method opens an $\mathrm{RAA}$ box, and when?
(g) True or false: a failed search shows that the sequent is not derivable.
(h) The goal is $R$ , and the resources are $P \vee Q$ , $P \to R$ , $Q \to S$ . Should the search be expected to succeed?
(i) Lines 3 and 4 are $Q \to R$ (a premise) and $Q$ . A searcher writes 5 $Q$ , assumption; 6 $R$ , $\mathrm{{\to}E}$ 3, 5; 7 $Q \to R$ , $\mathrm{{\to}I}$ 5–6; 8 $R$ , $\mathrm{{\to}E}$ 7, 4. Which refinements of the section does this break, and what single line replaces lines 5–8?
(j) Find a derivation of $P \vee Q, \ \neg P \vdash Q \vee R$ .
(k) Find a derivation of $(P \vee Q) \to R \vdash Q \to R$ .
(l) Find a derivation of $P \to (Q \to R), \ P \wedge \neg R \vdash \neg Q$ .

Solution.

(a) A box opened with $P \vee Q$ , with the goal $\bot$ .
(b) Two boxes: one on $P$ with the goal $Q$ , and one on $R$ with the goal $\bot$ .
(c) $P \wedge Q$ by $\mathrm{\wedge I}$ , then $\bot$ by $\mathrm{\neg E}$ .
(d) Step 2 postpones the goal. Step 3 needs $\neg P$ , which is not a resource, and making it a goal stalls. So step 5: $\mathrm{LEM}$ on $P$ , whose negation the resource waits for.
(e) 1, 3 and 6; not 4.
(f) Step 5, when steps 2–4 give nothing.
(g) False: it shows only that this search failed.
(h) No. $P$ false, $Q$ true, $R$ false, $S$ true makes every resource true and $R$ false, so the claim breaks. In $\mathrm{\vee E}$ , the case $Q$ gives only $S$ .
(i) Two refinements. Lines 7–8 are a detour ( $\mathrm{{\to}I}$ , then $\mathrm{{\to}E}$ on its own implication). Line 7 rebuilds a resource, and find the goal among the resources would have cited line 3. Replace lines 5–8 by 5 $R$ , $\mathrm{{\to}E}$ 3, 4.
(j) 3 $Q$ , $\mathrm{DS}$ 1, 2; 4 $Q \vee R$ , $\mathrm{\vee I}$ 3.
(k) 2 $Q$ , assumption, for $\mathrm{{\to}I}$ ; 3 $P \vee Q$ , $\mathrm{\vee I}$ 2; 4 $R$ , $\mathrm{{\to}E}$ 1, 3; 5 $Q \to R$ , $\mathrm{{\to}I}$ $2\text{–}4$ .
(l) 3 $P$ , $\mathrm{\wedge E}$ 2; 4 $\neg R$ , $\mathrm{\wedge E}$ 2; 5 $Q \to R$ , $\mathrm{{\to}E}$ 1, 3; 6 $\neg Q$ , $\mathrm{MT}$ 5, 4.

B. Practice

Exercise (B1: Three searches)

For each sequent, name the first goal-directed step, then find a derivation.

(a) $P \wedge (Q \to R) \vdash (P \to Q) \to R$ .
(b) $\neg(P \to Q) \vdash P \wedge \neg Q$ . Which conjunct does your derivation obtain by $\mathrm{RAA}$ , and which by $\mathrm{\neg I}$ alone?
(c) $\neg P \to Q \vdash P \vee Q$ .

Hint: in (c), look at what the premise is waiting for.

Solution.

(a) The goal is an implication: a box on $P \to Q$ with the goal $R$ , a letter. Step 3 splits the premise; its half $Q \to R$ gives $R$ once we have $Q$ , and the box’s assumption gives $Q$ once we have $P$ , which the premise’s other half supplies. So the chain runs backwards from $R$ to $Q$ to $P$ , and forwards it reads:
1 $P \wedge (Q \to R)$
2 $P \to Q$ asm, for $\mathrm{{{\to}}I}$
3 $P$ $\mathrm{{\wedge}E}$ 1
4 $Q$ $\mathrm{{{\to}}E}$ 2, 3
5 $Q \to R$ $\mathrm{{\wedge}E}$ 1
6 $R$ $\mathrm{{{\to}}E}$ 5, 4
7 $(P \to Q) \to R$ $\mathrm{{{\to}}I}$ 2–6
(b) The goal is a conjunction: two gaps, with goals $P$ and $\neg Q$ . The premise can be used only by $\mathrm{\neg E}$ , against $P \to Q$ , so in each gap we aim to manufacture $P \to Q$ . The goal $\neg Q$ is a negation: a box on $Q$ , where $P \to Q$ follows by a box that repeats $Q$ , and it clashes with the premise. The goal $P$ is a letter, and the resources give nothing, so step 5: $\mathrm{RAA}$ on $\neg P$ . Then $P \to Q$ follows by vacuous implication (Proposition 2.1.2, written VI), and it clashes with the premise. The conjunct $P$ is the one our derivation obtains by $\mathrm{RAA}$ ; $\neg Q$ needs only $\mathrm{\neg I}$ . (That no derivation of $P$ from the premise avoids $\mathrm{RAA}$ is true, but we do not prove it.)
1 $\neg (P \to Q)$
2 $\neg P$ asm, for $\mathrm{RAA}$
3 $P \to Q$ VI 2
4 $\bot$ $\mathrm{{\neg}E}$ 3, 1
5 $P$ $\mathrm{RAA}$ 2–4
6 $Q$ asm, for $\mathrm{{\neg}I}$
7 $P$ asm, for $\mathrm{{{\to}}I}$
8 $Q$ $\mathrm{R}$ 6
9 $P \to Q$ $\mathrm{{{\to}}I}$ 7–8
10 $\bot$ $\mathrm{{\neg}E}$ 9, 1
11 $\neg Q$ $\mathrm{{\neg}I}$ 6–10
12 $P \wedge \neg Q$ $\mathrm{{\wedge}I}$ 5, 11

Written with primitive rules only, line 3 becomes the four lines of a box on $P$ that clashes with $\neg P$ , writes $Q$ by $\mathrm{\bot E}$ , and closes by $\mathrm{{\to}I}$ ; the derivation then has 15 lines instead of 12.
(c) The goal is a disjunction, so step 2 postpones it; the premise is waiting for $\neg P$ , which is not a resource, and nothing clashes. Step 5, $\mathrm{LEM}$ on $P$ , the statement the premise is waiting for: in the case $P$ , $\mathrm{\vee I}$ gives the left side; in the case $\neg P$ , the premise gives $Q$ and $\mathrm{\vee I}$ the right side.

\neg P \to 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}

Q

\mathrm{{{\to}}E}

1, 5

P \vee Q

\mathrm{{\vee}I}

P \vee Q

\mathrm{{\vee}E}

2, 3–4, 5–7

The derivation has 8 lines. An $\mathrm{RAA}$ box on $\neg(P \vee Q)$ also works, with two manufactured clashes inside it.

Exercise (B2: The last step)

A search for $P \to Q, \ R \to \neg Q \vdash P \to \neg R$ has reached the stage below; only the last line is missing. Name the move, then complete it.

P \to Q

R \to \neg Q

P

asm, for

\mathrm{{{\to}}I}

Q

\mathrm{{{\to}}E}

1, 3

R

asm, for

\mathrm{{\neg}I}

\neg Q

\mathrm{{{\to}}E}

2, 5

\bot

\mathrm{{\neg}E}

4, 6

\neg R

\mathrm{{\neg}I}

5–7

\;\textbf{?}

Solution. The move is the chapter’s main one: the skeleton was read off the goal, and the gap was filled from both ends. The goal $P \to \neg R$ is an implication, so the outer box opened with $P$ (line 3); its new goal $\neg R$ is a negation, so the inner box opened with $R$ (line 5). The premises then met the goal in the middle: $\mathrm{{\to}E}$ at lines 4 and 6 gave $Q$ and $\neg Q$ , and the clash at line 7. The inner box was closed at line 8. What remains is to close the outer box on its goal, by $\mathrm{{\to}I}\ 3\text{–}8$ :

P \to Q

R \to \neg Q

P

asm, for

\mathrm{{{\to}}I}

Q

\mathrm{{{\to}}E}

1, 3

R

asm, for

\mathrm{{\neg}I}

\neg Q

\mathrm{{{\to}}E}

2, 5

\bot

\mathrm{{\neg}E}

4, 6

\neg R

\mathrm{{\neg}I}

5–7

P \to \neg R

\mathrm{{{\to}}I}

3–8

The box runs from its assumption $P$ , line 3, to its last line $\neg R$ , line 8, which lies in the outer box itself and not in the inner one, as $\mathrm{{\to}I}$ requires.

Exercise (B3: Two boxes and a chain)

Find a derivation of $P \to (Q \to R), \ P \to (R \to S) \vdash P \to (Q \to S)$ , and describe the search in three sentences, naming its goal-directed and premise-directed steps.

Solution.

P \to (Q \to R)

P \to (R \to S)

P

asm, for

\mathrm{{{\to}}I}

Q \to R

\mathrm{{{\to}}E}

1, 3

R \to S

\mathrm{{{\to}}E}

2, 3

Q

asm, for

\mathrm{{{\to}}I}

R

\mathrm{{{\to}}E}

4, 6

S

\mathrm{{{\to}}E}

5, 7

Q \to S

\mathrm{{{\to}}I}

6–8

P \to (Q \to S)

\mathrm{{{\to}}I}

3–9

The search: the goal is an implication, so a goal-directed step opens a box on $P$ with the goal $Q \to S$ , and a second goal-directed step opens a box on $Q$ with the goal $S$ . With $P$ a resource, premise-directed steps fire both premises by $\mathrm{{\to}E}$ , giving $Q \to R$ and $R \to S$ . Then a backward chain from the goal $S$ (it needs $R$ , which needs $Q$ , a resource) is written forwards as two more $\mathrm{{\to}E}$ lines, and the two boxes close in the reverse order of opening. (Lines 4 and 5 may equally be written inside the box of $Q$ .)

Exercise (B4: Cut the detours)

The derivation below of $P \wedge Q, \ Q \to R \vdash R \wedge P$ is correct but contains detours.

P \wedge Q

Q \to R

Q

\mathrm{{\wedge}E}

Q

asm, for

\mathrm{{{\to}}I}

R

\mathrm{{{\to}}E}

2, 4

Q \to R

\mathrm{{{\to}}I}

4–5

R

\mathrm{{{\to}}E}

6, 3

P

\mathrm{{\wedge}E}

R \wedge P

\mathrm{{\wedge}I}

7, 8

R

\mathrm{{\wedge}E}

R \wedge P

\mathrm{{\wedge}I}

10, 8

(a) Find each pair of lines in which a line is built by an introduction rule and taken apart at once by the matching elimination.
(b) Which line rebuilds a premise?
(c) Rewrite the derivation without the detours.
(d) To cut the $\mathrm{{\to}I}$ / $\mathrm{{\to}E}$ detour, the box is copied with a line in place of its assumption: which line, and what does the copy give?

Solution.

(a) Lines 6–7: $\mathrm{{\to}I}$ , then $\mathrm{{\to}E}$ on line 6. Lines 9–10: $\mathrm{\wedge I}$ , then $\mathrm{\wedge E}$ on line 9. (Line 11 then rebuilds line 9.)
(b) Line 6 is premise 2, rebuilt by a box. Find the goal among the resources would have cited line 2.
(c) Six lines instead of eleven:

1 $P \wedge Q$
2 $Q \to R$
3 $Q$ $\mathrm{{\wedge}E}$ 1
4 $R$ $\mathrm{{{\to}}E}$ 2, 3
5 $P$ $\mathrm{{\wedge}E}$ 1
6 $R \wedge P$ $\mathrm{{\wedge}I}$ 4, 5
(d) Line 3 takes the place of the assumption on line 4. The box’s one other line, “ $R$ , $\mathrm{{\to}E}$ 2, 4”, becomes “ $R$ , $\mathrm{{\to}E}$ 2, 3”, which is line 4 of (c).

C. Going deeper

Exercise (C1: The second half)

A search for $P \vee (Q \wedge R) \vdash (P \vee Q) \wedge (P \vee R)$ has used the premise by $\mathrm{\vee E}$ and finished the first case; the second case is blank. Name the move, then complete it.

P \vee (Q \wedge R)

P

asm, for

\mathrm{{\vee}E}

P \vee Q

\mathrm{{\vee}I}

P \vee R

\mathrm{{\vee}I}

(P \vee Q) \wedge (P \vee R)

\mathrm{{\wedge}I}

3, 4

Q \wedge R

asm, for

\mathrm{{\vee}E}

\vdots

(P \vee Q) \wedge (P \vee R)

(P \vee Q) \wedge (P \vee R)

\mathrm{{\vee}E}

1, 2–5, 6–11

Solution (Hint 1). The current goal of the blank box is a conjunction. What does step 2 do with it, and what does step 3 do with the box’s assumption?

Solution (Hint 2). Line 7 is $Q$ , by $\mathrm{\wedge E}$ from line 6.

Solution. The move is the chapter’s main one again: read the skeleton off the goal, then work from both ends. The current goal $(P \vee Q) \wedge (P \vee R)$ is a conjunction, so step 2 splits it into the goals $P \vee Q$ and $P \vee R$ , to be joined by $\mathrm{\wedge I}$ . Both are disjunctions, so they are postponed, and step 3 turns to the resource $Q \wedge R$ : $\mathrm{\wedge E}$ gives $Q$ and $R$ . Now each disjunction has a side that is a resource, so $\mathrm{\vee I}$ is safe.

P \vee (Q \wedge R)

P

asm, for

\mathrm{{\vee}E}

P \vee Q

\mathrm{{\vee}I}

P \vee R

\mathrm{{\vee}I}

(P \vee Q) \wedge (P \vee R)

\mathrm{{\wedge}I}

3, 4

Q \wedge R

asm, for

\mathrm{{\vee}E}

Q

\mathrm{{\wedge}E}

R

\mathrm{{\wedge}E}

P \vee Q

\mathrm{{\vee}I}

P \vee R

\mathrm{{\vee}I}

(P \vee Q) \wedge (P \vee R)

\mathrm{{\wedge}I}

9, 10

(P \vee Q) \wedge (P \vee R)

\mathrm{{\vee}E}

1, 2–5, 6–11

Both boxes end in the current goal of the $\mathrm{\vee E}$ , as that rule requires. Here $\mathrm{\vee I}$ adds $P$ on the left of $Q$ and of $R$ ; in the first case it added $Q$ and $R$ on the right of $P$ . Citing line 2 inside the second box would be the sibling-box error of Exercise (C2: Find the error, used later).

Exercise (C2: A disjunction from nothing)

(a) Derive $\vdash (P \to Q) \vee (Q \to P)$ .
(b) In a paragraph, say which step of your derivation uses $\mathrm{RAA}$ or $\mathrm{LEM}$ , and why the method cannot avoid step 5 on this goal.

Solution (Hint 1). The goal is a disjunction and there are no premises. Which steps of the method does that leave?

Solution (Hint 2). Step 5 has two forms. Which statement would make each side of the goal easy, if you knew whether it held?

Solution.

(a) $\mathrm{LEM}$ on $Q$ . In the case $Q$ , the implication $P \to Q$ holds by a box that repeats $Q$ . In the case $\neg Q$ , the implication $Q \to P$ holds by a box on $Q$ that clashes with $\neg Q$ , followed by $\mathrm{\bot E}$ .
1 $Q \vee \neg Q$ $\mathrm{LEM}$
2 $Q$ asm, for $\mathrm{{\vee}E}$
3 $P$ asm, for $\mathrm{{{\to}}I}$
4 $Q$ $\mathrm{R}$ 2
5 $P \to Q$ $\mathrm{{{\to}}I}$ 3–4
6 $(P \to Q) \vee (Q \to P)$ $\mathrm{{\vee}I}$ 5
7 $\neg Q$ asm, for $\mathrm{{\vee}E}$
8 $Q$ asm, for $\mathrm{{{\to}}I}$
9 $\bot$ $\mathrm{{\neg}E}$ 8, 7
10 $P$ $\mathrm{{\bot}E}$ 9
11 $Q \to P$ $\mathrm{{{\to}}I}$ 8–10
12 $(P \to Q) \vee (Q \to P)$ $\mathrm{{\vee}I}$ 11
13 $(P \to Q) \vee (Q \to P)$ $\mathrm{{\vee}E}$ 1, 2–6, 7–12

$\mathrm{LEM}$ on $P$ works equally well, with the roles of the two sides exchanged.
(b) $\mathrm{LEM}$ is used at line 1; $\mathrm{RAA}$ appears only inside the derivation of $\mathrm{LEM}$ (Proposition 2.5.3) that line 1 abbreviates. The method cannot avoid step 5 here. Step 2 postpones the $\vee$ goal; with no premises, step 3 has nothing to eliminate and step 4 nothing to clash; and $\mathrm{\vee I}$ cannot come first, because neither side follows from no premises (with $P$ true and $Q$ false, $P \to Q$ is false; with $P$ false and $Q$ true, $Q \to P$ is false; Chapter 4 turns such choices into proofs). So a resource must be created from nothing, and only step 5 does that. This shows that the method needs step 5; that every derivation of the sequent uses $\mathrm{RAA}$ or an equivalent is a stronger claim, which we do not prove.

Marking scheme. (10 points)

3: a correct split by $\mathrm{LEM}$ (on $Q$ or on $P$ ), with two case boxes combined by $\mathrm{\vee E}$ , or a correct $\mathrm{RAA}$ box on the negated goal.
2: in one case, the implication by a box that repeats the case assumption.
2: in the other case, the implication by a box that clashes with the case assumption, then $\mathrm{\bot E}$ , or by VI (Proposition 2.1.2).
1: $\mathrm{\vee I}$ on the correct side in each case, every citation available.
2: the paragraph names the $\mathrm{LEM}$ line (or the $\mathrm{RAA}$ line) and explains why no other step of the method applies.

Fatal errors (0 for the step): choosing a side of the goal before the split; citing one case’s assumption in the other case. A correct derivation by $\mathrm{RAA}$ on the negated goal earns full marks: its 2 + 2 + 1 points go to the two implications derived inside the $\mathrm{RAA}$ box (one by a box that repeats an assumption, one by a clash and $\mathrm{\bot E}$ , or by VI (Proposition 2.1.2) once $\neg Q$ or $\neg P$ has been derived) and to the $\mathrm{\vee I}$ lines that clash with the $\mathrm{RAA}$ assumption.

Exercise (C3: Exit check: search)

Find a derivation of $\neg(\neg P \wedge Q) \vdash P \vee \neg Q$ by the method of this section. Write one sentence for each step of the method you take, and point to the classical step of your derivation.

Solution. The search.

Step 1. The premise $\neg(\neg P \wedge Q)$ on top, the goal $P \vee \neg Q$ at the bottom, one gap.
Step 2. The goal is a disjunction, so it is postponed: the premise does not say which side holds.
Step 3. Nothing can be eliminated. The premise is a negation, so it can be used only in a clash (step 4), against $\neg P \wedge Q$ , and we do not have it.
Step 4. The goal is not $\bot$ , and nothing clashes. We are stuck.
Step 5. We assume the negation of the goal, $\neg(P \vee \neg Q)$ , with the new goal $\bot$ .
Step 4, inside the box. The new assumption clashes with $P \vee \neg Q$ , which $\mathrm{\vee I}$ builds from either side. The side $P$ is a letter that nothing gives; the side $\neg Q$ is a negation, which step 2 can build. So $\neg Q$ becomes the goal: a box on $Q$ , with the goal $\bot$ . Choosing a side is safe here, since the disjunction is manufactured for a clash with a resource that is its negation (step 4 allows either side when the disjunction is built for a clash with its own negation).
Step 4, in the box on $Q$ . The resources are the premise, the assumption of step 5, and $Q$ . We aim at the premise: $\neg P \wedge Q$ becomes the goal, and step 2 splits it. Its half $Q$ is a resource; its half $\neg P$ is a negation: a box on $P$ , with the goal $\bot$ .
Step 4, in the box on $P$ . $\mathrm{\vee I}$ builds $P \vee \neg Q$ from $P$ , which clashes with the assumption of step 5. Now the boxes close from the inside out: $\neg P$ , then $\neg P \wedge Q$ , which clashes with the premise; then $\neg Q$ , then $P \vee \neg Q$ , which clashes with the assumption of step 5; and $\mathrm{RAA}$ closes the outer box.

\neg (\neg P \wedge Q)

\neg (P \vee \neg Q)

asm, for

\mathrm{RAA}

Q

asm, for

\mathrm{{\neg}I}

P

asm, for

\mathrm{{\neg}I}

P \vee \neg Q

\mathrm{{\vee}I}

\bot

\mathrm{{\neg}E}

5, 2

\neg P

\mathrm{{\neg}I}

4–6

\neg P \wedge Q

\mathrm{{\wedge}I}

7, 3

\bot

\mathrm{{\neg}E}

8, 1

\neg Q

\mathrm{{\neg}I}

3–9

P \vee \neg Q

\mathrm{{\vee}I}

\bot

\mathrm{{\neg}E}

11, 2

P \vee \neg Q

\mathrm{RAA}

2–12

The classical step is line 13, the $\mathrm{RAA}$ that closes the box of line 2; every other box closes by $\mathrm{\neg I}$ . The assumption of line 2 is used twice, at lines 6 and 12, just as in Example (A search that reaches step 5 at once).

A second route. Step 5 may take its other form: $\mathrm{LEM}$ on $P$ . In the case $P$ , $\mathrm{\vee I}$ gives the goal. In the case $\neg P$ , the goal’s side $\neg Q$ is a negation: a box on $Q$ builds $\neg P \wedge Q$ , which clashes with the premise, so $\neg Q$ , and $\mathrm{\vee I}$ . That derivation has 11 lines, and its classical step is the $\mathrm{LEM}$ line.

Marking scheme. (10 points)

2: step 2 postpones the disjunctive goal, with the reason (neither side is in hand).
2: steps 3 and 4 find that the premise can be used only by producing $\neg P \wedge Q$ for a clash.
2: step 5 is chosen: $\mathrm{RAA}$ on the whole goal, or $\mathrm{LEM}$ on $P$ . ( $\mathrm{LEM}$ on $Q$ also works; our route with it then uses a second classical step, an $\mathrm{RAA}$ for $P$ in the case $Q$ ; award it.) A classical derived rule used at step 3, such as DM (d) on the premise followed by $\mathrm{\neg\neg E}$ , is also accepted; its DM (d) and $\mathrm{\neg\neg E}$ lines are the classical lines, and naming either earns the point.
3: the inner boxes and their clashes are correct, and every citation is available.
1: the classical line is named.

Fatal errors (0 for the step): $\mathrm{\vee I}$ as the last line, from a disjunct derived from the premise alone; on the $\mathrm{RAA}$ route, an $\mathrm{RAA}$ box on the whole goal opened with anything but $\neg(P \vee \neg Q)$ .

Exercise (C4: Two sequents that look alike)

Derive each sequent, and say which of your two derivations needed the classical rule.

(a) $\neg(P \wedge Q), \ P \vdash \neg Q$ .
(b) $\neg(P \wedge \neg Q), \ P \vdash Q$ .

Then explain why, in (b), the natural $\mathrm{\neg I}$ box on $\neg Q$ ends at $\neg\neg Q$ and not at $Q$ .

Solution.

(a) The goal is a negation: a $\mathrm{\neg I}$ box on $Q$ , in which $P \wedge Q$ clashes with the first premise.
1 $\neg (P \wedge Q)$
2 $P$
3 $Q$ asm, for $\mathrm{{\neg}I}$
4 $P \wedge Q$ $\mathrm{{\wedge}I}$ 2, 3
5 $\bot$ $\mathrm{{\neg}E}$ 4, 1
6 $\neg Q$ $\mathrm{{\neg}I}$ 3–5
(b) The goal $Q$ is a letter, and the resources give nothing directly, so step 5: $\mathrm{RAA}$ , a box on $\neg Q$ , in which $P \wedge \neg Q$ clashes with the first premise.

\neg (P \wedge \neg Q)

P

\neg Q

asm, for

\mathrm{RAA}

P \wedge \neg Q

\mathrm{{\wedge}I}

2, 3

\bot

\mathrm{{\neg}E}

4, 1

Q

\mathrm{RAA}

3–5

The derivation of (b) needed the classical rule, at line 6; the derivation of (a) did not. The two have the same shape, and the difference is the goal. In (a) it is a negation, which $\mathrm{\neg I}$ builds. In (b) it is a letter, and the box that reaches $\bot$ opens with $\neg Q$ ; $\mathrm{\neg I}$ writes the negation of a box’s assumption, so closing that box by $\mathrm{\neg I}$ gives $\neg\neg Q$ , and our derivation reaches $Q$ with the classical rule instead: $\mathrm{RAA}$ in place of $\mathrm{\neg I}$ (or $\mathrm{\neg\neg E}$ after it).

3.1.1. The moves so far

3.1.2. Partial derivations

3.1.3. The method

3.1.4. Splitting the goal

3.1.5. Cases must end in the goal

3.1.6. Postponing a disjunction

3.1.7. When nothing else works

3.1.8. Four refinements

3.1.9. A search that fails

3.1.10. A mathematical goal

3.1.11. The rules in one place

3.1.12. Exercises

A. Check your understanding

B. Practice

C. Going deeper