1.4 Proving an Implication: the Rule of the Box

Sections 1.2 and 1.3 gave three rules. $\mathrm{\wedge I}$ builds a conjunction; $\mathrm{\wedge E}$ and $\mathrm{{\to}E}$ take a line apart or use it. With them we can use an implication, but we cannot prove one. This section fills that gap with the rule $\mathrm{{\to}I}$ . The rule asks us to do something new: to assume a statement we do not know, inside a boundary that says where the assumption holds. The boundary is a box. With the box we can name the error of Argument B, and say exactly which earlier lines a line may cite.

1.4.1. Supposing something we do not know

Here is a small theorem about a real number $x$ .

If $x > 2$ , then $x^2 > 4$ .

The proof everyone would write goes like this. Suppose $x > 2$ . Then $x > 0$ , so multiplying $x > 2$ by $x$ gives $x^2 > 2x$ . Also $2x > 4$ . Hence $x^2 > 4$ . Then, often without saying it: this proves that if $x > 2$ , then $x^2 > 4$ .

Look at the first sentence. We do not know that $x > 2$ . The number $x$ is arbitrary, and it may well be $0$ . So “suppose $x > 2$ ” asserts nothing. It opens a temporary world, one in which $x > 2$ holds, and asks what else holds there.

Inside that world, the sentences “ $x^2 > 2x$ ”, “ $2x > 4$ ”, and “ $x^2 > 4$ ” are true. Outside it they are not: at $x = 0$ all three are false. Only the last sentence of the proof leaves the temporary world. What it carries out is not “ $x^2 > 4$ ” but the implication “if $x > 2$ , then $x^2 > 4$ ”, and that is true for every real $x$ .

None of the rules so far can do this: $\mathrm{\wedge I}$ writes a conjunction, and $\mathrm{\wedge E}$ and $\mathrm{{\to}E}$ write a piece of a line that is already there. To prove “if $x > 2$ , then $x^2 > 4$ ” from nothing, we must be allowed to suppose.

A supposition is only safe if it has a boundary. Without one, the proof above could go on: “… Hence $x^2 > 4$ . So $x^2 > 4$ for every real $x$ .” That is false at $x = 0$ . The error is not in any computation; it is that a sentence from inside the temporary world was used outside it.

A derivation draws the boundary as a box. The assumption opens the box: it is written with a vertical bar to its left and a short horizontal rule under it. Every line derived under the assumption carries the same bar. When the box closes, the bar stops, and exactly one thing leaves: the implication from the assumption to the box’s last line.

To prove “if $\varphi$ , then $\psi$ ”, assume $\varphi$ in a box, reach $\psi$ inside it, and close the box.

1.4.2. The introduction rule for implication

From now on the given part of a schema may also be a box, cited as a range of lines from its first line to its last; nothing else in Definition 1.2.1 changes.

Here is the rule, as a pattern. Beside it, for reference, is the rule $\mathrm{{\to}E}$ of Definition 1.3.1, so that the two rules for “implies” stand in one place.

Definition 1.4.1 (Rules for Implication)

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

The left schema is the rule $\mathrm{{\to}I}$ (implication-introduction); the right one is $\mathrm{{\to}E}$ (Definition 1.3.1). In $\mathrm{{\to}I}$ , the line $\varphi$ is an assumption, which opens the box, and the assumption is discharged when the box closes. The line $\psi$ is a line of that box itself, not of a box inside it.

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

Open a box whose first line is the assumption $\varphi$ . The assumption may be any statement: true or false, related to the premises or not. Its justification is “assumption”, printed “asm, for $\mathrm{{\to}I}$ ”: the annotation names the rule that will close the box. The price of assuming anything we like is the box.
Inside the box, work as usual. Every rule may be used. A line inside may cite the assumption and every earlier line that is not inside a box that has already closed: the premises, the lines above the box that are still in force, and the lines derived inside the box so far.
The last line of the box is $\psi$ . It must be a line of this box itself, not a line of some further box opened inside it. (The drawing cannot show this, which is why the definition says it in words.)
Close the box, and write $\varphi \to \psi$ on a later line outside it, in practice the very next line. The justification cites the whole box as the range $i\text{–}j$ , from its assumption to its last line, not its lines one by one.
After the box closes, nothing inside it may be cited again. The assumption is discharged, and everything derived under it goes with it. Only the implication leaves.

Clause 5 is the boundary of the temporary world. The subsection “Which lines a line may cite” below turns clause 5 into an exact rule.

What each box is for. From now on every assumption says, in its justification column, what its box is for. “asm, for $\mathrm{{\to}I}$ ” says that the box was opened to prove an implication, and that a $\mathrm{{\to}I}$ line will close it. In a written proof the same line is the word “suppose”. While a derivation is still growing and its closing line is not yet written, the annotation records the plan.

Second readingA box of one line

The degenerate case is $i = j$ : a box of one line, whose assumption is also its last line. Then $\psi$ is $\varphi$ , and the rule writes $\varphi \to \varphi$ . Nothing in the rule asks the box to contain more than its assumption.

Why the rule is right. The implication $\varphi \to \psi$ claims only that $\psi$ holds whenever $\varphi$ does. The box shows exactly that: starting from $\varphi$ , and from facts that hold anyway, the rules lead to $\psi$ .

Why the box closes. The lines inside hold only under the assumption. If the assumption is false, as $x > 2$ is at $x = 0$ , they may be false too. Closing the box is what stops them being used where the assumption is not in force.

1.4.3. A first box: implication is transitive

The first result proved with a box is the chaining of implications. Section 1.3 used chains of implications forwards, firing each on a hypothesis already in hand. Here the hypothesis is not in hand, and we still want the chain.

Proposition 1.4.1 (Implication Is Transitive)

$P \to Q, \ Q \to R \vdash P \to R$ .

Idea. Start from the goal. Its main connective is $\to$ , so the last line will be $\mathrm{{\to}I}$ , and that needs a box that opens with $P$ and ends with $R$ . Inside the box, the new goal is $R$ . Reason backwards: $R$ is the conclusion of the premise $Q \to R$ , so $\mathrm{{\to}E}$ gives it once $Q$ is on a line. And $Q$ is the conclusion of $P \to Q$ , so $\mathrm{{\to}E}$ gives it from $P$ , which the box has just assumed.

In the Givens/Goal table, $\mathrm{{\to}I}$ moves the hypothesis into the Givens and makes the conclusion the goal.

Givens	Goal
$P \to Q$ , $Q \to R$	$P \to R$
$P \to Q$ , $Q \to R$ , $P$ (box opened)	$R$
$P \to Q$ , $Q \to R$ , $P$ , $Q$ ( $\mathrm{{\to}E}$ )	$R$
$P \to Q$ , $Q \to R$ , $P$ , $Q$ , $R$ ( $\mathrm{{\to}E}$ )	$R$ ✓

The same search as a growing derivation: the box opened, its goal $R$ at the bottom (left); then line 4 written forwards (right).

P \to Q

Q \to R

P

asm, for

\mathrm{{{\to}}I}

\vdots

R

P \to R

\mathrm{{{\to}}I}

3–5

P \to Q

Q \to R

P

asm, for

\mathrm{{{\to}}I}

Q

\mathrm{{{\to}}E}

1, 3

\vdots

R

P \to R

\mathrm{{{\to}}I}

3–5

Proof. The following derivation has premises $P \to Q$ and $Q \to R$ , and last line $P \to R$ .

P \to Q

Q \to R

P

asm, for

\mathrm{{{\to}}I}

Q

\mathrm{{{\to}}E}

1, 3

R

\mathrm{{{\to}}E}

2, 4

P \to R

\mathrm{{{\to}}I}

3–5

Line 3 opens a box with the assumption $P$ . Lines 4 and 5 apply $\mathrm{{\to}E}$ inside it, each citing a premise and a line of the box. Line 5, $R$ , is the last line of the box. Line 6 closes it and writes $P \to R$ , citing the box $3\text{–}5$ . By Definition 1.2.3, this proves the proposition.

Read the drawing once more. The bar that starts at line 3 stops after line 5. The statements $P$ , $Q$ , and $R$ on lines 3–5 were never established outright; they hold inside the temporary world where $P$ is assumed. Only $P \to R$ stands outside, next to the premises.

Now give the letters some content. Let $x$ be a real number, and let $P : x > 3, \qquad Q : x^2 > 9, \qquad R : x^2 > 4 .$ The premise $P \to Q$ holds: when $x > 3$ , we have $x > 0$ , so $x^2 = x \cdot x > 3x > 9$ . The premise $Q \to R$ holds because $4 < 9$ : if $x^2 > 9$ , then $x^2 > 4$ . With the premises in hand, lines 3–6 become a paragraph, one sentence per line.

Line	Sentence
3	Suppose $x > 3$ .
4	Since $x > 3$ implies $x^2 > 9$ , we get $x^2 > 9$ .
5	Since $x^2 > 9$ implies $x^2 > 4$ , we get $x^2 > 4$ .
6	Hence, if $x > 3$ , then $x^2 > 4$ .

A practiced writer would compress this to “if $x > 3$ , then $x^2 > 9 > 4$ ”: the same derivation with its joints hidden. When a proof is hard to follow, expanding it back into this form is how one finds the gap.

Remark. The same result holds with the two premises joined into one, $(P \to Q) \wedge (Q \to R) \vdash P \to R$ . Two $\mathrm{\wedge E}$ lines take the premise apart first (premise-directed), and the rest is the derivation above, renumbered.

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

P \to Q

\mathrm{{\wedge}E}

Q \to R

\mathrm{{\wedge}E}

P

asm, for

\mathrm{{{\to}}I}

Q

\mathrm{{{\to}}E}

2, 4

R

\mathrm{{{\to}}E}

3, 5

P \to R

\mathrm{{{\to}}I}

4–6

1.4.4. Argument B, diagnosed

Section 1.1 broke the form of Argument B’s last step. Here is the rule B misused. With $E$ : “ $n$ is even” and $S$ : “ $n^2$ is even”, B’s prose is this derivation.

E

asm, for

\mathrm{{{\to}}I}

S

algebra 1

E \to S

\mathrm{{{\to}}I}

1–2

Line 1 is B’s “Suppose $n$ is even, say $n = 2k$ ”. Line 2 is its computation $n^2 = 4k^2 = 2(2k^2)$ , a step of algebra, as in Example (A product of numbers in the unit interval). Line 3 is what the box earns; set it beside what B claimed.

Diagram. Labels: what B's box earns, E, S, E to S, what B claimed, S to E

B’s box opens with $E$ and closes on $S$ , so $\mathrm{{\to}I}$ lets it write $E \to S$ : the converse of the claim. B’s last sentence wrote $S \to E$ . The rule asks the box to open with the hypothesis of the implication being proved, here $S$ , and B never opened that box.

The repair fails. Keep $E \to S$ , open a box with $S$ , and inside it use $S$ to reach $E$ : that step goes from $E \to S$ and $S$ to $E$ . It is affirming the consequent, the bad form of Section 1.3. Try to break it. Take “if $x > 2$ , then $x^2 > 4$ ” and “ $x^2 > 4$ ”. At $x = -3$ both are true, since $9 > 4$ , and “ $x > 2$ ” is false. So B cannot be saved by moving its lines around: a $\mathrm{{\to}I}$ proof of $S \to E$ opens its box with $S$ .

Warning. The box of $\mathrm{{\to}I}$ opens with the hypothesis of the implication to be proved, never with its conclusion: Argument B used $\mathrm{{\to}I}$ with the box opened at the wrong end.

Quick check. A proof of “if $x^3 > 8$ , then $x > 2$ ” begins “Suppose $x > 2$ .” and ends “Hence $x^3 > 8$ .” What does its box earn? Is the claim it was meant to prove true?

Solution. Its box opens with $x > 2$ and closes on $x^3 > 8$ , so it earns $(x > 2) \to (x^3 > 8)$ , the converse of the claim. The claim itself is true: if $x \le 2$ , then $x^3 \le 2^3 = 8$ , since a larger real number has a larger cube, so $x^3 > 8$ forces $x > 2$ . But this box does not prove it.

Second readingTwo errors that cancel

Example (Two errors that cancel)

Let $x$ be a real number. Here is a “proof” that if $x > 3$ , then $x^2 > 9$ : Suppose $x^2 > 9$ . Then $x > 3$ . Hence, if $x > 3$ , then $x^2 > 9$ . Is the conclusion true? Is it proved?

Solution. As a derivation, the “proof” reads as follows.

x^2 > 9

asm, for

\mathrm{{{\to}}I}

x > 3

algebra 1

(x > 3) \to (x^2 > 9)

\mathrm{{{\to}}I}

1–2

Two lines fail. Line 2 is no fact about numbers: at $x = -4$ we have $x^2 = 16 > 9$ , and $x > 3$ fails. Line 3 writes the converse of what the box earns. The box opens with $x^2 > 9$ and ends with $x > 3$ , so $\mathrm{{\to}I}$ would write $(x^2 > 9) \to (x > 3)$ .

The two errors cancel. The implication the box would earn is false, and reversed it is the true claim: if $x > 3$ , then $x > 0$ , so $x^2 = x \cdot x > 3x > 9$ . A reader who compares only the last line with the claim sees nothing wrong; a checker who reads every line finds both errors. A correct conclusion is no evidence that the lines above it are correct.

1.4.5. A box must end on a line of its own

Try to derive $\vdash P \to (Q \to P)$ . The goal is an implication, so open a box with $P$ ; the new goal $Q \to P$ is again an implication, so open a box with $Q$ inside the first. The statement $P$ is already on line 1, so it is tempting to close the inner box at once.

P

asm, for

\mathrm{{{\to}}I}

Q

asm, for

\mathrm{{{\to}}I}

Q \to P

\mathrm{{{\to}}I}

2–2

P \to (Q \to P)

\mathrm{{{\to}}I}

1–3

A checker reads the box $2\text{–}2$ : its assumption is $Q$ , and its last line is $Q$ . So $\mathrm{{\to}I}$ may write only $Q \to Q$ from it, and line 3 is rejected. The statement $P$ stands on line 1, outside the inner box, and clause 3 asks for $\psi$ as a line of the box itself.

The fix is bookkeeping: copy $P$ into the inner box. Copying an available line is the rule $\mathrm{R}$ (repetition), made official as clause (D3) of the definition below. The copy “ $P$ , R 1” then ends the inner box.

Some books let a box end on any line available inside it. This book copies the line in, so that every $\mathrm{{\to}I}$ line can be checked by looking only at the box it cites. The corrected derivation is Example (First boxes) (b) below.

1.4.6. Which lines a line may cite

In a derivation without boxes (Definition 1.2.2), a line may cite any earlier line. With boxes that is no longer enough: after the derivation of Proposition 1.4.1, a line 7 citing line 5 would write $R$ outside the box, the “ $x^2 > 4$ for every $x$ ” error of the first subsection. What matters is which earlier lines are still available, and the bars show it.

A line inside a box may be cited only from inside that box. Once a box has closed above you, nothing inside it can be cited; the boxes you are in may be left across their tops, and passing beside a closed box is fine.

Open a box, close a box: an assumption lives exactly as long as its box.

A whole box, cited by $\mathrm{{\to}I}$ , has its own condition: the citing line must stand in exactly the boxes that the cited box stands in, other than the cited box itself. For single lines:

a line in no box is available at every later line;
a line inside a box is available further down that box, and inside every box opened within it;
once its box closes, the line is available nowhere.

The figure shows eleven lines without statements: box A is lines 2–4, box B lines 6–10, and box C, lines 7–8, sits inside B. An arrow runs from a citing line up to the line it cites, solid and marked $\checkmark$ if legal, dashed and marked $\times$ if not. A bracket on the left marks a whole box cited.

A line can be cited from below only while every box containing it is still open. Line 8 leaves box C across its top to cite line 6, and line 11 passes beside the closed box B to cite line 5. Lines 5 and 11 stand in no box, and neither do the boxes A and B they cite whole.

Quick check. In the figure, which of lines 1–9 may line 10 cite?

Solution. Lines 1, 5, 6 and 9. Lines 1 and 5 are in no box; lines 6 and 9 are in box B, which contains line 10. Lines 2–4 are not available (box A has closed), and neither are lines 7–8 (box C has closed). It may also cite the whole box 7–8, which, like line 10, stands in box B alone.

Here is the official version, the one a checker uses.

Definition 1.4.2 (Derivation)

Fix a list of rules. A derivation is a finite list of numbered lines $1, 2, \dots, n$ , each carrying one statement and a justification, together with a set of boxes. A box is a block of consecutive lines whose first line is an assumption. Any two boxes are either disjoint or one inside the other. A box ends at one of its lines and is closed after it. The last line of the derivation lies outside every box.

The scope rule. Line $i$ is available at line $k$ if $i < k$ and every box containing line $i$ also contains line $k$ . A box is available at line $k$ if it ends before line $k$ and the boxes other than itself that contain it are exactly the boxes containing line $k$ . A line may cite only lines and boxes available at it.

Every line is exactly one of the following:

(D1) a premise; the premises are the first lines, above every box, with a short rule under the last of them;
(D2) an assumption, which may be any statement, and opens a new box;
(D3) a repetition of the statement on a line available at this one, justified “R” and the line repeated;
(D4) the conclusion of one rule of the list, applied to lines and boxes available at this one, such that this line and the cited lines and boxes form an instance of the rule’s schema.

Clause (D3) is the rule $\mathrm{R}$ (repetition), whose schema is

i

\varphi

\vdots

k

\varphi

\mathrm{R}

i

where line $i$ must be available at line $k$ .

(D1)–(D4) say: given, assumed, copied, or one step of one rule, always from what is still available.

The scope rule is the definition’s real content: line $i$ is available at line $k$ when every assumption that line $i$ was derived under is still in force at line $k$ : the picture rule above, in words a checker can apply.

Second readingWhy checking stays mechanical

Well defined. Whether a line is available is decided by looking at the boxes; nothing about the meaning of the statements enters. Checking a derivation stays mechanical.

Nothing earlier changes. A derivation with no boxes is a box-free derivation of Definition 1.2.2 for the same rules with $\mathrm{R}$ added: with no boxes, “available” means just “earlier”. So every derivation of Sections 1.2 and 1.3 is a derivation in the new sense, and Definition 1.2.3 is read from now on with this definition. The sequent $\Gamma \vdash \psi$ still means: there is a derivation whose premises all belong to $\Gamma$ and whose last line is $\psi$ . Its last line lies in no box, so it depends on the premises and on nothing that was merely assumed.

Second readingMore on repetition

The typical use of $\mathrm{R}$ copies a line into a box opened below it.

i

\varphi

\vdots

j

\psi

asm, for

\mathrm{{{\to}}I}

\vdots

k

\varphi

\mathrm{R}

i

Line $i$ is available at line $k$ exactly when every box containing line $i$ contains line $k$ ; in this drawing, line $i$ is in no box that has closed, so the copy is legal. The worked example Example (First boxes) below uses it.

Warning. A box that is never closed cannot end a derivation. If the last line of a list is still inside a box, it depends on an assumption that was never discharged, and Definition 1.4.2 does not count the list as a derivation at all. “Suppose $x > 2$ . Then $x^2 > 4$ ”, with nothing after it, proves nothing about $x$ : the implication is the only thing the supposition was allowed to produce, and it was never written.

1.4.7. How to check a derivation

Section 1.2 checked a line by asking which rule it uses, which lines it cites, and whether they are earlier. With boxes the third question becomes: are they available here? For each line after the premises, ask:

Which rule? Name it. An assumption opens a box; $\mathrm{R}$ repeats; every other line applies one rule.
Which lines or boxes does it cite, and do they form an instance of the rule’s schema? $\mathrm{{\to}E}$ cites an implication and exactly its hypothesis; $\mathrm{{\to}I}$ cites one box, whose assumption and last line must be the two sides of the implication written.
Are they available here? Apply the scope rule to each cited line and box.

Finding a derivation may need an idea; checking one never does. Here is the check run on the derivation of Proposition 1.4.1.

Line	Which rule?	Cites	Available?
1, 2	premises (D1)	—	—
3	assumption (D2); opens the box 3–5	—	—
4	$\mathrm{{\to}E}$ : $Q$ from $P \to Q$ and $P$	1, 3	1 is in no box; 3 is in box 3–5, which contains 4
5	$\mathrm{{\to}E}$ : $R$ from $Q \to R$ and $Q$	2, 4	2 is in no box; 4 is in box 3–5, which contains 5
6	$\mathrm{{\to}I}$ : $P \to R$ from the box	box 3–5	the box ended at 5; neither it nor 6 lies in another box

Every line passes, and the last line lies in no box. The bar shows the temporary world: it starts at line 3 and stops after line 5.

1.4.8. An assumption used outside its box

Now watch the scope rule catch an error. Take the derivation of Proposition 1.4.1 and add one careless line.

Example (A line cited from a closed box)

Is the following a derivation? If it were, what would it show?

P \to Q

Q \to R

P

asm, for

\mathrm{{{\to}}I}

Q

\mathrm{{{\to}}E}

1, 3

R

\mathrm{{{\to}}E}

2, 4

P \to R

\mathrm{{{\to}}I}

3–5

R

\mathrm{R}

Solution. No. Lines 1–6 are the derivation of Proposition 1.4.1, and line 7 claims to be a repetition (D3). Line 5 lies inside the box $3\text{–}5$ , and that box does not contain line 7. By the scope rule, line 5 is not available at line 7, and (D3) repeats only an available line. So line 7 is illegal.

If it were allowed, the list would show $P \to Q, \ Q \to R \vdash R$ , and that would be a disaster. Let $x$ be a real number, and take $P$ : “ $x > 3$ ”, $Q$ : “ $x > 2$ ”, $R$ : “ $x > 1$ ”. Both premises are true whatever $x$ is. At $x = 0$ the conclusion $x > 1$ is false. A step that leads from true premises to a false conclusion cannot be a step of proof.

Warning. The assumption of a closed box is gone, and so is everything derived from it. Here is a typical slip. “Suppose $x > 1$ . Then $x^2 = x \cdot x > 1 \cdot x > 1$ . Hence $x > 1$ implies $x^2 > 1$ . Moreover $x^3 = x \cdot x^2 > 1$ , so $x^3 > 1$ .” The sentence “Hence …” closed the box. The last sentence still uses $x > 1$ and $x^2 > 1$ , and so it asserts $x^3 > 1$ with no hypothesis, which fails at $x = 0$ . The repair is to keep the box open until everything that needs $x > 1$ is done, and to conclude “if $x > 1$ , then $x^2 > 1$ and $x^3 > 1$ ”.

Quick check. In the derivation below, which of lines 3 to 7 may cite line 2 individually?

P \to Q

P

asm, for

\mathrm{{{\to}}I}

Q

\mathrm{{{\to}}E}

1, 2

P \wedge Q

\mathrm{{\wedge}I}

2, 3

Q \wedge P

\mathrm{{\wedge}I}

3, 2

P \to (Q \wedge P)

\mathrm{{{\to}}I}

2–5

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

\mathrm{{\wedge}I}

1, 6

Solution. Lines 3, 4, and 5. They lie in the box $2\text{–}5$ , the only box containing line 2, so line 2 is available to each of them. Line 6 cites the box $2\text{–}5$ as a whole, which is what $\mathrm{{\to}I}$ requires; it does not cite line 2 by itself, and could not, since line 6 is outside the box. Line 7 may not cite line 2 either, for the same reason.

1.4.9. More boxes: from nothing, and one inside another

Example (First boxes)

Find a derivation of each sequent.

(a) $\vdash P \to P$ .
(b) $\vdash P \to (Q \to P)$ .
(c) $P \to (Q \to R) \vdash Q \to (P \to R)$ .

Solution.

(a) Idea. The goal is an implication, so open a box with its hypothesis $P$ ; the box must end with $P$ . The assumption is already $P$ , so the box can end at once: a box of one line, whose assumption is also its last line. Nothing in $\mathrm{{\to}I}$ asks a box to contain more than its assumption.
1 $P$ asm, for $\mathrm{{{\to}}I}$
2 $P \to P$ $\mathrm{{{\to}}I}$ 1–1

Line 1 is an assumption (D2) and opens the box $1\text{–}1$ , whose last line is $P$ . Line 2 cites that box, which ended before line 2 and, like line 2, lies in no other box. There are no premises, so this shows $\vdash P \to P$ . It is the first statement in the book derivable from no premises by the rules of logic alone. Argument B’s box in “Argument B, diagnosed” also began without premises, but it used a step of algebra. Every other rule so far (Definition 1.2.5, Definition 1.3.1, and $\mathrm{R}$ of Definition 1.4.2) cites at least one earlier line, so without a box a derivation must start with a premise. A box is what escapes: its first line is an assumption, and the assumption is discharged before the end.
(b) Idea. This is the derivation the checker accepted after the fix in “A box must end on a line of its own”: line 3 copies $P$ into the inner box.
1 $P$ asm, for $\mathrm{{{\to}}I}$
2 $Q$ asm, for $\mathrm{{{\to}}I}$
3 $P$ $\mathrm{R}$ 1
4 $Q \to P$ $\mathrm{{{\to}}I}$ 2–3
5 $P \to (Q \to P)$ $\mathrm{{{\to}}I}$ 1–4

Line 3 is legal: the only box containing line 1, the box $1\text{–}4$ , also contains line 3. The boxes are nested, and the inner one closes first. No line cites line 2 on its own: the assumption $Q$ is never used, and nothing in $\mathrm{{\to}I}$ requires it to be. An implication whose conclusion is already known holds whatever its hypothesis.
(c) Idea. The goal $Q \to (P \to R)$ asks for a box with $Q$ and, inside it, a box with $P$ ending in $R$ . Inside both boxes, work from the premise: its main connective is the first $\to$ , with hypothesis $P$ , so $\mathrm{{\to}E}$ fires on the assumption $P$ and gives $Q \to R$ . That implication fires on the assumption $Q$ and gives $R$ , the inner goal.

Both boxes opened, goals at their feet (left); then the inner lines written, and only line 7 still to justify (right).

P \to (Q \to R)

Q

asm, for

\mathrm{{{\to}}I}

P

asm, for

\mathrm{{{\to}}I}

\vdots

R

P \to R

Q \to (P \to R)

P \to (Q \to R)

Q

asm, for

\mathrm{{{\to}}I}

P

asm, for

\mathrm{{{\to}}I}

Q \to R

\mathrm{{{\to}}E}

1, 3

R

\mathrm{{{\to}}E}

4, 2

P \to R

\mathrm{{{\to}}I}

3–5

Q \to (P \to R)

The finished derivation:

P \to (Q \to R)

Q

asm, for

\mathrm{{{\to}}I}

P

asm, for

\mathrm{{{\to}}I}

Q \to R

\mathrm{{{\to}}E}

1, 3

R

\mathrm{{{\to}}E}

4, 2

P \to R

\mathrm{{{\to}}I}

3–5

Q \to (P \to R)

\mathrm{{{\to}}I}

2–6

Line 5 cites line 2 from inside the inner box: every box containing line 2 (only $2\text{–}6$ ) contains line 5. So the order of two hypotheses does not matter. For real numbers $a$ and $x$ , the derivation turns “if $a > 0$ , then (if $x > 1$ , then $ax > a$ )” into “if $x > 1$ , then (if $a > 0$ , then $ax > a$ )”.

In (b) and (c) the goal told us which boxes to open, and in which order: the outermost $\to$ of the goal gives the outermost box. This is the goal-directed move of this section. An implication goal opens a box with its hypothesis; the new goal is its conclusion.

1.4.10. Two hypotheses, or one at a time

A theorem with two hypotheses, “if $x > 0$ and $y > 0$ , then $xy > 0$ ”, is often written with one hypothesis at a time: “let $x > 0$ ; then, if $y > 0$ , $xy > 0$ ”. The two forms are $(P \wedge Q) \to R$ and $P \to (Q \to R)$ . Each can be derived from the other, so a writer may use whichever reads better.

Proposition 1.4.2 (Two Hypotheses or One at a Time)

$(P \wedge Q) \to R \vdash P \to (Q \to R)$ , and $P \to (Q \to R) \vdash (P \wedge Q) \to R$ .

Try it first (ten minutes): for the first claim, which boxes will you open, and in which order?

Idea. The tempting first move is premise-directed: use $(P \wedge Q) \to R$ at once. But $\mathrm{{\to}E}$ needs $P \wedge Q$ on a line, and at the start nothing is on a line except the premise. So start from the goal. Its main connective is the first $\to$ , so open a box with $P$ ; the new goal $Q \to R$ is again an implication, so open a box with $Q$ inside the first. Now both $P$ and $Q$ are available, $\mathrm{\wedge I}$ builds $P \wedge Q$ , and the premise fires. For the second claim the goal $(P \wedge Q) \to R$ asks for one box, with $P \wedge Q$ ; take the assumption apart and feed the halves to the premise one at a time, $P$ first because it is the premise’s outer hypothesis.

The first claim: the outer box opened (left), then the inner one, with goal $R$ (right).

(P \wedge Q) \to R

P

asm, for

\mathrm{{{\to}}I}

\vdots

Q \to R

P \to (Q \to R)

\mathrm{{{\to}}I}

2–6

(P \wedge Q) \to R

P

asm, for

\mathrm{{{\to}}I}

Q

asm, for

\mathrm{{{\to}}I}

\vdots

R

Q \to R

\mathrm{{{\to}}I}

3–5

P \to (Q \to R)

\mathrm{{{\to}}I}

2–6

The second claim: the box opened (left), then the assumption taken apart (right).

P \to (Q \to R)

P \wedge Q

asm, for

\mathrm{{{\to}}I}

\vdots

R

(P \wedge Q) \to R

\mathrm{{{\to}}I}

2–6

P \to (Q \to R)

P \wedge Q

asm, for

\mathrm{{{\to}}I}

P

\mathrm{{\wedge}E}

Q

\mathrm{{\wedge}E}

\vdots

R

(P \wedge Q) \to R

\mathrm{{{\to}}I}

2–6

Before reading on: in the first derivation, which lines may line 4 cite, and why may line 6 cite the box 3–5 but not line 5 on its own?

Proof. For the first claim, the following is a derivation with premise $(P \wedge Q) \to R$ and last line $P \to (Q \to R)$ .

(P \wedge Q) \to R

P

asm, for

\mathrm{{{\to}}I}

Q

asm, for

\mathrm{{{\to}}I}

P \wedge Q

\mathrm{{\wedge}I}

2, 3

R

\mathrm{{{\to}}E}

1, 4

Q \to R

\mathrm{{{\to}}I}

3–5

P \to (Q \to R)

\mathrm{{{\to}}I}

2–6

Line 4 may cite lines 1, 2, and 3: line 1 lies in no box, the only box containing line 2 (the box $2\text{–}6$ ) contains line 4, and both boxes containing line 3 contain line 4. Line 6 may cite the box $3\text{–}5$ , because that box has ended and both it and line 6 lie in the box $2\text{–}6$ and in no other. Line 6 may not cite line 5 on its own, because the box $3\text{–}5$ contains line 5 and not line 6.

For the second claim, the following is a derivation with premise $P \to (Q \to R)$ and last line $(P \wedge Q) \to R$ .

P \to (Q \to R)

P \wedge Q

asm, for

\mathrm{{{\to}}I}

P

\mathrm{{\wedge}E}

Q

\mathrm{{\wedge}E}

Q \to R

\mathrm{{{\to}}E}

1, 3

R

\mathrm{{{\to}}E}

5, 4

(P \wedge Q) \to R

\mathrm{{{\to}}I}

2–6

Lines 3–6 cite line 1, which lies in no box, or earlier lines of the box $2\text{–}6$ , from inside that box. Line 7 cites the box $2\text{–}6$ , which has ended, and neither that box nor line 7 lies in any other box. By Definition 1.2.3, the two derivations prove the two claims.

Quick check. In the second derivation of Proposition 1.4.2, what does the annotation of line 2 say, and which line closes its box?

Solution. “asm, for $\mathrm{{\to}I}$ ”: the box was opened to prove an implication. Line 7 closes it, citing the box $2\text{–}6$ .

In the first derivation the boxes are nested, and the inner one closes first: an assumption made later is discharged earlier. That is the general pattern, forced by Definition 1.4.2, since two boxes are either disjoint or one inside the other.

Read mathematically, the first claim turns “if $x > 0$ and $y > 0$ , then $xy > 0$ ” into “if $x > 0$ , then (if $y > 0$ , then $xy > 0$ )”, and the second turns it back. The two forms say the same thing, one hypothesis at a time or both at once.

Quick check. To show $Q \wedge R \vdash (P \to Q) \wedge (S \to R)$ , does the derivation need one box or two?

Solution. Two. The goal’s main connective is $\wedge$ , which opens no box, so the goal splits into the two implications $P \to Q$ and $S \to R$ (goal-directed $\mathrm{\wedge I}$ ). Each is proved by $\mathrm{{\to}I}$ , with its own box, opened by its own hypothesis. Inside each box, $\mathrm{\wedge E}$ on the premise gives the half that box needs.

Q \wedge R

P

asm, for

\mathrm{{{\to}}I}

Q

\mathrm{{\wedge}E}

P \to Q

\mathrm{{{\to}}I}

2–3

S

asm, for

\mathrm{{{\to}}I}

R

\mathrm{{\wedge}E}

S \to R

\mathrm{{{\to}}I}

5–6

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

\mathrm{{\wedge}I}

4, 7

The two boxes are disjoint: the first closes before the second opens. Line 8 may cite lines 4 and 7, which lie in no box.

1.4.11. The rule card

Before the card, the rule at work on large statements. Each row is one use of $\mathrm{{\to}I}$ : the box, and the line it writes.

Example (Instances of

\mathrm{{\to}I}

)

$\varphi$	$\psi$	The box	New line
$P \wedge \neg Q$	$P \wedge (P \wedge \neg Q)$	from $P \wedge \neg Q$ (asm) to $P \wedge (P \wedge \neg Q)$ , by $\mathrm{\wedge E}$ and then $\mathrm{\wedge I}$	$(P \wedge \neg Q) \to (P \wedge (P \wedge \neg Q))$
$Q \to R$	$(P \to Q) \to (P \to R)$	from $Q \to R$ (asm) to $(P \to Q) \to (P \to R)$ , with two boxes inside it	$(Q \to R) \to ((P \to Q) \to (P \to R))$
$(P \vee Q) \wedge R$	$(P \vee Q) \wedge R$	a box of one line	$((P \vee Q) \wedge R) \to ((P \vee Q) \wedge R)$

Not an instance. A box opens with $Q$ and ends with $P$ , copied in by $\mathrm{R}$ . The line “ $P \to Q$ — $\mathrm{{\to}I}$ ” is not an instance: $\mathrm{{\to}I}$ writes the assumption first, $Q \to P$ . This is Argument B’s step.

The card grows by two rows. In Shape, “box $\varphi$ … $\psi$ ” is a closed box from the assumption $\varphi$ to its last line $\psi$ .

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`

In the Lean column, intro hp opens the box and names its assumption hp.

Warning (Not allowed: $\mathrm{{\to}I}$ ). Each step below is wrong; the tag names the clause of the rule’s reading that it breaks.

Close the box on a line of a box inside it: clause 3, the last line must be a line of the box itself (“A box must end on a line of its own”).
Write $\psi \to \varphi$ from a box that runs from $\varphi$ to $\psi$ : clause 4, the box opens with the hypothesis (Argument B).
Cite a line inside a closed box: clause 5 (Example (A line cited from a closed box)).
End the derivation inside an open box: clause 4, the box must close (the warning on a box that is never closed).
Cite the box’s lines one by one: clause 4, the box is cited whole, as a range.

The discharge is where the rule bites, so here is one wrong step beside the right one, with premises $(P \wedge R) \to Q$ and $R$ . On the left, line 6 carries $Q$ out of the box by repetition, as if $P$ had been proved. On the right, line 6 closes the box with $\mathrm{{\to}I}$ .

(P \wedge R) \to Q

R

P

asm, for

\mathrm{{{\to}}I}

P \wedge R

\mathrm{{\wedge}I}

3, 2

Q

\mathrm{{{\to}}E}

1, 4

Q

\mathrm{R}

(P \wedge R) \to Q

R

P

asm, for

\mathrm{{{\to}}I}

P \wedge R

\mathrm{{\wedge}I}

3, 2

Q

\mathrm{{{\to}}E}

1, 4

P \to Q

\mathrm{{{\to}}I}

3–5

The left list would show $(P \wedge R) \to Q, \ R \vdash Q$ . Let $x$ be a real number, with $P$ : “ $x > 5$ ”, $R$ : “ $x > 0$ ”, $Q$ : “ $x > 3$ ”. The first premise holds for every $x$ , and at $x = 1$ both premises are true and $Q$ is false.

The sentence for $\mathrm{{\to}I}$ is the one to watch. “Assume $P$ ” opens a box, and “hence $Q$ ” is its last line. The closing line, “so $P$ implies $Q$ ”, is usually left unsaid in written mathematics. It is still there: the box closes whether or not anyone says so. It is also the line Argument B got wrong.

Remark (Looking ahead). Chapter 2 proves the claim Argument B wanted, with the rules for “not”.

1.4.12. Exercises

A. Check your understanding

Exercise (A1)

Consider the following derivation, whose justifications are missing.

P \to (Q \to R)

Q

P

asm, for

\mathrm{{{\to}}I}

Q \to R

(i)

R

(ii)

P \to R

(iii)

(a) Write the schema of $\mathrm{{\to}I}$ from memory, and state the condition that the drawing cannot show.
(b) Fill in the justifications (i), (ii), (iii), and say what the derivation shows, written with $\vdash$ .
(c) Which of lines 1–5 are available at line 6, and which boxes?
(d) Someone extends the derivation by a line 7, the statement $R$ justified by $\mathrm{{\to}E}$ 6, 3. Is the result a derivation? If not, name the clause of Definition 1.4.2 that line 7 breaks.
(e) In the first derivation in the proof of Proposition 1.4.2, why is line 4 available at line 5? And why is the inner box closed before the outer one?
(f) In the same derivation, which rule produces line 5, and which lines does it cite?

Solution.

(a) The schema is the left one in Definition 1.4.1: a box from an assumption $\varphi$ on line $i$ to a line $\psi$ on line $j$ , and then $\varphi \to \psi$ on line $k$ , justified $\mathrm{{\to}I}$ $i\text{–}j$ . The condition the drawing cannot show: $\psi$ is a line of that box itself, not of a box inside it.
(b)
- (i) $\mathrm{{\to}E}$ 1, 3; (ii) $\mathrm{{\to}E}$ 4, 2; (iii) $\mathrm{{\to}I}$ $3\text{–}5$ . The derivation shows $P \to (Q \to R), \ Q \vdash P \to R$ .
(c) Lines 1 and 2, and the box $3\text{–}5$ . Lines 3, 4, and 5 lie in the box $3\text{–}5$ , which does not contain line 6, so none of them is available there one by one. The box as a whole is available at line 6: it has ended, and neither it nor line 6 lies in another box. That is why (iii) may cite it.
(d) No. Line 6 is available at line 7, but line 3 is not: it lies in the box $3\text{–}5$ , which does not contain line 7. So line 7 applies a rule to a line that is not available, which (D4) forbids.
(e) Line 4 lies in two boxes, $2\text{–}6$ and $3\text{–}5$ , and both contain line 5; so by the scope rule line 4 is available at line 5. The inner box $3\text{–}5$ lies inside the outer box $2\text{–}6$ , and two boxes are either disjoint or one inside the other, so the inner box must end first. Read off the goal: the inner box proves $Q \to R$ , which is the last line the outer box needs.
(f) $\mathrm{{\to}E}$ , citing line 1, the implication $(P \wedge Q) \to R$ , and line 4, its hypothesis $P \wedge Q$ .

Exercise (A2: Drill)

The parts run from one step, through a missing line, a justification column and steps to judge, to short derivations. Parts (e)–(g) refer to the eleven-line figure in “Which lines a line may cite”.

(a) A box runs from line 3, $(P \vee Q) \wedge R$ , to line 6, $S \to P$ , a line of that box itself. What does “ $\mathrm{{\to}I}$ 3–6” write?
(b) Line 7 is $(P \to Q) \to R$ , justified “ $\mathrm{{\to}I}$ 2–6”. What is line 2, and what does its annotation read?
(c) Line 9 is $(P \wedge Q) \to (R \vee S)$ , justified “ $\mathrm{{\to}I}$ 4–8”. What are lines 4 and 8?
(d) Say which lines below are premises and which are assumptions, and fill in (i) and (ii).

1 $P$
2 $Q$ asm, for $\mathrm{{{\to}}I}$
3 $P \wedge Q$ (i)
4 $Q \to (P \wedge Q)$ (ii)
(e) May line 8 cite line 5?
(f) May line 9 cite the whole box 2–4?
(g) May line 11 cite line 6?
(h) A box runs from line 3, $P$ (an assumption), to line 6, $R$ ; line 4, inside it, is $Q$ . Is “7. $P \to Q$ — $\mathrm{{\to}I}$ 3–4” correct?
(i) Find the illegal line, and say why it is illegal.

1 $P \to Q$
2 $P$ asm, for $\mathrm{{{\to}}I}$
3 $Q$ $\mathrm{{{\to}}E}$ 1, 2
4 $P \to Q$ $\mathrm{{{\to}}I}$ 2–3
5 $Q$ $\mathrm{{{\to}}E}$ 4, 2
(j) Let $x$ be a real number. Is “Suppose $x > 3$ . Then $x^2 > 9$ .”, with nothing after it, a proof that $x^2 > 9$ ?
(k) Show $\vdash (P \wedge Q) \to (Q \wedge P)$ by a derivation. Then write the argument as a paragraph of prose, one sentence per line.
(l) Derive $P \to Q \vdash (P \wedge R) \to Q$ .
(m) Derive $Q \vdash (P \wedge R) \to (Q \wedge R)$ .
(n) Derive $\vdash (P \wedge Q) \to (R \to P)$ . Which box opens first?
(o) Derive $(P \to Q) \wedge R \vdash P \to (Q \wedge R)$ .

Solution.

(a) $((P \vee Q) \wedge R) \to (S \to P)$ : the assumption on the left, the box’s last line on the right.
(b) Line 2 is $P \to Q$ , the hypothesis of line 7, and its annotation reads “asm, for $\mathrm{{\to}I}$ ”.
(c) Line 4 is the assumption $P \wedge Q$ , which opens the box; line 8 is $R \vee S$ , the last line of that box.
(d) Line 1 is a premise and line 2 an assumption; (i) $\mathrm{\wedge I}$ 1, 2; (ii) $\mathrm{{\to}I}$ $2\text{–}3$ .
(e) Yes: line 5 lies in no box.
(f) No: box 2–4 stands in no box, and line 9 stands in box B, so the two do not stand in exactly the same boxes.
(g) No: line 6 is inside box B, which closed after line 10.
(h) No: lines 3–4 are not a box, since the box runs on to line 6. $\mathrm{{\to}I}$ cites the whole box $3\text{–}6$ and writes $P \to R$ . ( $P \to Q$ is earned by a box of its own that ends on $Q$ .)
(i) Line 5: it cites line 2, which lies inside the box $2\text{–}3$ , closed before line 5.
(j) No. The box opened by “suppose” never closes, so nothing has left it; and at $x = 0$ the sentence $x^2 > 9$ is false. What the two sentences can prove, once the box closes, is “if $x > 3$ , then $x^2 > 9$ ”.
(k) The goal is an implication, so open a box with $P \wedge Q$ ; inside, $\mathrm{\wedge E}$ gives both halves, and $\mathrm{\wedge I}$ rebuilds them in the other order.

1 $P \wedge Q$ asm, for $\mathrm{{{\to}}I}$
2 $P$ $\mathrm{{\wedge}E}$ 1
3 $Q$ $\mathrm{{\wedge}E}$ 1
4 $Q \wedge P$ $\mathrm{{\wedge}I}$ 3, 2
5 $(P \wedge Q) \to (Q \wedge P)$ $\mathrm{{{\to}}I}$ 1–4

In prose: Assume $P$ and $Q$ . In particular, $P$ holds. In particular, $Q$ holds. Hence $Q$ and $P$ both hold. This proves that if $P$ and $Q$ , then $Q$ and $P$ . Compared with Proposition 1.2.1, the premise $P \wedge Q$ has become an assumption, and the conclusion has become an implication that depends on nothing.
(l) 2 $P \wedge R$ , assumption, for $\mathrm{{\to}I}$ ; 3 $P$ , $\mathrm{\wedge E}$ 2; 4 $Q$ , $\mathrm{{\to}E}$ 1, 3; 5 $(P \wedge R) \to Q$ , $\mathrm{{\to}I}$ $2\text{–}4$ .
(m) 2 $P \wedge R$ , assumption, for $\mathrm{{\to}I}$ ; 3 $R$ , $\mathrm{\wedge E}$ 2; 4 $Q \wedge R$ , $\mathrm{\wedge I}$ 1, 3; 5 $(P \wedge R) \to (Q \wedge R)$ , $\mathrm{{\to}I}$ $2\text{–}4$ .
(n) The box of $P \wedge Q$ opens first, since the goal’s main connective is its first $\to$ : 1 $P \wedge Q$ , assumption, for $\mathrm{{\to}I}$ ; 2 $R$ , assumption, for $\mathrm{{\to}I}$ , opening a box inside the first; 3 $P$ , $\mathrm{\wedge E}$ 1; 4 $R \to P$ , $\mathrm{{\to}I}$ $2\text{–}3$ ; 5 $(P \wedge Q) \to (R \to P)$ , $\mathrm{{\to}I}$ $1\text{–}4$ .
(o) 2 $P$ , assumption, for $\mathrm{{\to}I}$ ; 3 $P \to Q$ , $\mathrm{\wedge E}$ 1; 4 $Q$ , $\mathrm{{\to}E}$ 3, 2; 5 $R$ , $\mathrm{\wedge E}$ 1; 6 $Q \wedge R$ , $\mathrm{\wedge I}$ 4, 5; 7 $P \to (Q \wedge R)$ , $\mathrm{{\to}I}$ $2\text{–}6$ .

B. Practice

Exercise (B1: Two boxes, one inside the other)

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

(P \wedge Q) \to R

S \to Q

S

asm, for

\mathrm{{{\to}}I}

P

asm, for

\mathrm{{{\to}}I}

\vdots

\vdots

S \to (P \to R)

Solution. The move is goal-directed, twice: an implication goal opens a box with its hypothesis, and the new goal is its conclusion. The goal $S \to (P \to R)$ gave the outer box, with $S$ , and its conclusion $P \to R$ gave the inner box, with $P$ ; the inner goal is $R$ . Inside both boxes, work backwards from the first premise: $R$ is its conclusion, so it suffices to build its hypothesis $P \wedge Q$ exactly. $P$ is line 4, and $Q$ comes from the second premise and the assumption $S$ .

(P \wedge Q) \to R

S \to Q

S

asm, for

\mathrm{{{\to}}I}

P

asm, for

\mathrm{{{\to}}I}

Q

\mathrm{{{\to}}E}

2, 3

P \wedge Q

\mathrm{{\wedge}I}

4, 5

R

\mathrm{{{\to}}E}

1, 6

P \to R

\mathrm{{{\to}}I}

4–7

S \to (P \to R)

\mathrm{{{\to}}I}

3–8

Every citation is available. Lines 1 and 2 lie in no box. Line 3 lies only in the box $3\text{–}8$ , which contains line 5. Lines 4, 5 and 6 lie in both boxes, which contain lines 6 and 7. Line 8 cites the box $4\text{–}7$ , which has ended and stands, like line 8, in the box $3\text{–}8$ and no other. Line 9 cites the box $3\text{–}8$ , which has ended and, like line 9, lies in no other box.

Exercise (B2: An assumption that is not used)

(a) Show that $Q \vdash P \to Q$ , and say which line needs repetition.
(b) Show that $\vdash (P \wedge Q) \to (R \to Q)$ .
(c) Let $x$ be a real number. Write the instance of (a) with $Q$ : “ $x^2 \ge 0$ ” and $P$ : “ $x > 5$ ” as an English sentence, and say which hypothesis its proof never uses.

Solution.

(a) The goal is an implication, so open a box with $P$ ; its last line must be $Q$ .
1 $Q$
2 $P$ asm, for $\mathrm{{{\to}}I}$
3 $Q$ $\mathrm{R}$ 1
4 $P \to Q$ $\mathrm{{{\to}}I}$ 2–3

Line 3 needs repetition: $\mathrm{{\to}I}$ wants $Q$ as a line of the box $2\text{–}3$ itself. It is legal because line 1 lies in no box.
(b) Two implications, so two nested boxes: one with $P \wedge Q$ , and inside it one with $R$ .
1 $P \wedge Q$ asm, for $\mathrm{{{\to}}I}$
2 $Q$ $\mathrm{{\wedge}E}$ 1
3 $R$ asm, for $\mathrm{{{\to}}I}$
4 $Q$ $\mathrm{R}$ 2
5 $R \to Q$ $\mathrm{{{\to}}I}$ 3–4
6 $(P \wedge Q) \to (R \to Q)$ $\mathrm{{{\to}}I}$ 1–5

Line 4 is legal: the only box containing line 2 also contains line 4. (Applying $\mathrm{\wedge E}$ to line 1 inside the inner box works as well.)
(c) “ $x^2 \ge 0$ ; therefore, if $x > 5$ , then $x^2 \ge 0$ .” The hypothesis $x > 5$ is never used: its box only repeats what was known.

Exercise (B3: Unwinding an absolute value)

(a) Show that $P \to Q, \ P \to R \vdash P \to (Q \wedge R)$ .
(b) Let $x$ be a real number. Use (a) to deduce “if $\left| x - 2 \right| < 1$ , then $1 < x < 3$ ” from the two facts “if $\left| x - 2 \right| < 1$ , then $1 < x$ ” and “if $\left| x - 2 \right| < 1$ , then $x < 3$ ”. Write the resulting argument as prose.

Solution.

(a) The goal is an implication, so assume $P$ , and reach $Q \wedge R$ by getting each half.
1 $P \to Q$
2 $P \to R$
3 $P$ asm, for $\mathrm{{{\to}}I}$
4 $Q$ $\mathrm{{{\to}}E}$ 1, 3
5 $R$ $\mathrm{{{\to}}E}$ 2, 3
6 $Q \wedge R$ $\mathrm{{\wedge}I}$ 4, 5
7 $P \to (Q \wedge R)$ $\mathrm{{{\to}}I}$ 3–6

The assumption on line 3 is cited twice, by lines 4 and 5: a line is not used up when it is cited.
(b) Take $P$ : “ $\left| x - 2 \right| < 1$ ”, $Q$ : “ $1 < x$ ” and $R$ : “ $x < 3$ ”. The two facts are the premises $P \to Q$ and $P \to R$ , and $Q \wedge R$ is $(1 < x) \wedge (x < 3)$ , which $1 < x < 3$ abbreviates (Section 1.1). The derivation in (a), with these statements put in for the letters, is a derivation of $P \to (Q \wedge R)$ from the two facts.

In prose: Suppose $\left| x - 2 \right| < 1$ . Then $1 < x$ by the first fact, and $x < 3$ by the second. Hence $1 < x < 3$ . This proves that $\left| x - 2 \right| < 1$ implies $1 < x < 3$ .

Exercise (B4: Putting a derivation in order)

Here are nine lines, each a statement with its justification. Seven of them, in the right order and with the right boxes, form a derivation of $P \to (Q \to R) \vdash Q \to (P \to R)$ . Give the order, and say where each box opens and closes. Then say why each of the other two lines cannot be used.

(i) $P \to R$ , by $\mathrm{{\to}I}$ on the box from $P$ to $R$ .
(ii) $Q$ , assumption, for $\mathrm{{\to}I}$ .
(iii) $R$ , by $\mathrm{{\to}E}$ from $Q \to R$ and $Q$ .
(iv) $R$ , by $\mathrm{R}$ , repeating the line $R$ of (iii), written directly below (i).
(v) $P \to (Q \to R)$ , premise.
(vi) $Q \to (P \to R)$ , by $\mathrm{{\to}I}$ on the box from $Q$ to $P \to R$ .
(vii) $R$ , assumption, opening the box for the $\mathrm{{\to}I}$ that proves $P \to R$ .
(viii) $Q \to R$ , by $\mathrm{{\to}E}$ from $P \to (Q \to R)$ and $P$ .
(ix) $P$ , assumption, for $\mathrm{{\to}I}$ .

Solution. The order is (v), (ii), (ix), (viii), (iii), (i), (vi), with one box opened by (ii) and closed after (i), and a second box inside it, opened by (ix) and closed after (iii). This is the derivation of Example (First boxes) (c).

It is the only admissible order. The premise (v) comes first. The last line (vi) needs a box from $Q$ to $P \to R$ , so (ii) opens a box whose last line is (i). Line (i) needs a box from $P$ to $R$ , which must lie inside the box of $Q$ , since (i) is a line of that box; so (ix) opens the inner box, whose last line is (iii). Inside it, (viii) needs the premise and (ix), and (iii) needs (viii) and (ii). Opening the box of $P$ first and the box of $Q$ inside it would not do: the inner $\mathrm{{\to}I}$ would then give $Q \to R$ , and the outer one $P \to (Q \to R)$ , the premise again.

(iv) cannot be used where it is placed. Directly below (i), the inner box has closed, and line (iii) lies inside it; so (iii) is not available there, and (D3) repeats only an available line (the scope rule of Definition 1.4.2). It is the error of Example (A line cited from a closed box).
(v) cannot be used. $\mathrm{{\to}I}$ proves $P \to R$ from a box opened by $P$ , the hypothesis. A box opened by $R$ would prove an implication with hypothesis $R$ : the converse error of Argument B.

C. Going deeper

Exercise (C1: Exit check: a line from a closed box)

A student wants to show $(P \wedge Q) \to R \vdash (P \to (Q \to R)) \wedge (Q \to (P \to R))$ , and offers the following derivation. Lines 1–7 are the first derivation in the proof of Proposition 1.4.2.

(P \wedge Q) \to R

P

asm, for

\mathrm{{{\to}}I}

Q

asm, for

\mathrm{{{\to}}I}

P \wedge Q

\mathrm{{\wedge}I}

2, 3

R

\mathrm{{{\to}}E}

1, 4

Q \to R

\mathrm{{{\to}}I}

3–5

P \to (Q \to R)

\mathrm{{{\to}}I}

2–6

Q

asm, for

\mathrm{{{\to}}I}

P

asm, for

\mathrm{{{\to}}I}

R

\mathrm{R}

P \to R

\mathrm{{{\to}}I}

9–10

Q \to (P \to R)

\mathrm{{{\to}}I}

8–11

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

\mathrm{{\wedge}I}

7, 12

(a) Find the first illegal line, and name the clause of Definition 1.4.2 that it breaks.
(b) Is the student’s conclusion derivable from the premise? Justify your answer.
(c) The student defends line 10: “at line 10, both $P$ and $Q$ are assumed, exactly as they were at line 5, so $R$ holds there too.” Explain why Definition 1.4.2 does not accept this defense, and show by an instance with real numbers that the move “repeat a line of a closed box” cannot be allowed.

Solution (Hint 1). For (a), check each line’s citations against the scope rule; for (b), keep the student’s idea and change one step.

Solution (Hint 2). For (b), inside the box of $P$ at line 9, the assumptions $Q$ (line 8) and $P$ (line 9) are both available. What did lines 4 and 5 do with such a pair?

Solution.

(a) Line 10 is the first illegal line. It claims to repeat line 5 by (D3), but line 5 lies in the boxes $2\text{–}6$ and $3\text{–}5$ , and neither contains line 10. So line 5 is not available at line 10, and (D3) allows repeating only an available line. Lines 1–9 are correct, and lines 11–13 would be correct if line 10 were.
(b) Yes: the sequent is derivable. Replace line 10 by two lines that do inside the new boxes what lines 4 and 5 did inside the old ones.

1 $(P \wedge Q) \to R$
2 $P$ asm, for $\mathrm{{{\to}}I}$
3 $Q$ asm, for $\mathrm{{{\to}}I}$
4 $P \wedge Q$ $\mathrm{{\wedge}I}$ 2, 3
5 $R$ $\mathrm{{{\to}}E}$ 1, 4
6 $Q \to R$ $\mathrm{{{\to}}I}$ 3–5
7 $P \to (Q \to R)$ $\mathrm{{{\to}}I}$ 2–6
8 $Q$ asm, for $\mathrm{{{\to}}I}$
9 $P$ asm, for $\mathrm{{{\to}}I}$
10 $P \wedge Q$ $\mathrm{{\wedge}I}$ 9, 8
11 $R$ $\mathrm{{{\to}}E}$ 1, 10
12 $P \to R$ $\mathrm{{{\to}}I}$ 9–11
13 $Q \to (P \to R)$ $\mathrm{{{\to}}I}$ 8–12
14 $(P \to (Q \to R)) \wedge (Q \to (P \to R))$ $\mathrm{{\wedge}I}$ 7, 13

Every box containing line 8 or line 9 contains line 10, and line 1 lies in no box; the other lines check as before. The student’s derivation was wrong and its conclusion right: a flawed argument can have a true conclusion.
(c) Availability is about boxes, not about which statements happen to be assumed. The boxes $8\text{–}11$ and $9\text{–}10$ of the student’s derivation are new boxes; that their assumptions repeat those of the old boxes gives line 10 no access to what was derived inside the old ones. And the move, once allowed, can be used anywhere. Used outside every box, as a line 8 “ $R$ , R 5” after lines 1–7, it would derive $(P \wedge Q) \to R \vdash R$ . Let $x$ be a real number, and take $P$ : “ $x > 2$ ”, $Q$ : “ $x > 3$ ” and $R$ : “ $x > 1$ ”. The premise “if $x > 2$ and $x > 3$ , then $x > 1$ ” is true whatever $x$ is, and at $x = 0$ the conclusion $x > 1$ is false. A move that leads from a true premise to a false conclusion cannot be a step of proof.

Marking scheme. (10 points)

3: names line 10, because line 5 lies in boxes that do not contain it.
3: gives any correct derivation of the sequent, every citation available.
1: says the conclusion is derivable although the argument is wrong.
3: explains that availability depends on boxes, not on repeated assumptions, with an instance where the move leads from a true premise to a false conclusion.

Fatal errors (0 for the step): naming line 5 or line 9; claiming the sequent is not derivable; refuting the conclusion instead of the move.

Exercise (C2: A hypothesis inside a hypothesis)

Show that $(P \to Q) \to (P \to R) \vdash P \to (Q \to R)$ . Then say, in one sentence, why the premise cannot be used until a third box is opened.

Solution (Hint 1). Read the boxes off the goal. The premise’s hypothesis is $P \to Q$ : what would you need to derive it?

Solution (Hint 2). Start: line 2 assumes $P$ and line 3 assumes $Q$ , read off the goal. The last line of the box of $Q$ must be $R$ , and line 1 gives $P \to R$ only once $P \to Q$ is on an available line.

Solution. The goal $P \to (Q \to R)$ asks for a box with $P$ and, inside it, a box with $Q$ whose last line is $R$ . The premise gives $P \to R$ as soon as we have $P \to Q$ , and $P \to R$ with the available $P$ gives $R$ . So the task is to derive $P \to Q$ inside the box of $Q$ , and that takes a third box.

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

P

asm, for

\mathrm{{{\to}}I}

Q

asm, for

\mathrm{{{\to}}I}

P

asm, for

\mathrm{{{\to}}I}

Q

\mathrm{R}

P \to Q

\mathrm{{{\to}}I}

4–5

P \to R

\mathrm{{{\to}}E}

1, 6

R

\mathrm{{{\to}}E}

7, 2

Q \to R

\mathrm{{{\to}}I}

3–8

P \to (Q \to R)

\mathrm{{{\to}}I}

2–9

Line 5 is a legal repetition: both boxes containing line 3 contain line 5. Line 8 may cite line 2 because the box $2\text{–}9$ , the only box containing line 2, contains line 8.

The sentence: the premise fires only on an available line $P \to Q$ , and no available line is $P \to Q$ or has it as a conjunct or as the conclusion of an implication, so it can come only from $\mathrm{{\to}I}$ , which needs a box of its own.

Line 1 does not help, since $\mathrm{{\to}E}$ on it would need $P \to Q$ already. The third box assumes $P$ again although line 2 already did: $\mathrm{{\to}I}$ needs the box, not new information.

Marking scheme. (10 points)

2: opens a box with $P$ and inside it a box with $Q$ , read off the goal.
3: derives $P \to Q$ inside the box of $Q$ by a box whose last line is $Q$ .
2: obtains $P \to R$ , then $R$ , by $\mathrm{{\to}E}$ on available lines.
2: closes the boxes inner first, each $\mathrm{{\to}I}$ citing an available box.
1: the sentence says $P \to Q$ must be a line that no elimination rule can supply, hence needs a box.

Fatal errors (0 for the step): citing a line outside the box that contains it; writing $P \to Q$ with no box.

Exercise (C3: Exit check: a derivation and its prose)

(a) Write a derivation of $P \to Q, \ (Q \to R) \wedge (R \to S) \vdash P \to S$ , with every line justified.
(b) Let $x$ be a real number, and take $P$ : “ $x > 5$ ”, $Q$ : “ $x > 4$ ”, $R$ : “ $x^2 > 16$ ”, $S$ : “ $x^2 > 9$ ”. Say why each premise is true for every real $x$ . Then write your derivation as fluent prose about $x$ , one sentence per step.

Solution.

(a) Premise-directed first: the second premise is a conjunction, so $\mathrm{\wedge E}$ takes it apart. Goal-directed next: the goal is an implication, so open a box with its hypothesis $P$ , and reach $S$ by firing the three implications in turn.
1 $P \to Q$
2 $(Q \to R) \wedge (R \to S)$
3 $Q \to R$ $\mathrm{{\wedge}E}$ 2
4 $R \to S$ $\mathrm{{\wedge}E}$ 2
5 $P$ asm, for $\mathrm{{{\to}}I}$
6 $Q$ $\mathrm{{{\to}}E}$ 1, 5
7 $R$ $\mathrm{{{\to}}E}$ 3, 6
8 $S$ $\mathrm{{{\to}}E}$ 4, 7
9 $P \to S$ $\mathrm{{{\to}}I}$ 5–8

Lines 1–4 lie in no box, so they are available inside the box $5\text{–}8$ ; line 9 cites that box, which has ended, and neither it nor line 9 lies in another box.
(b) The premise $P \to Q$ holds because $5 > 4$ : if $x > 5$ , then $x > 4$ . For $Q \to R$ : if $x > 4$ , then $x > 0$ , so $x^2 = x \cdot x > 4x > 16$ . For $R \to S$ : if $x^2 > 16$ , then $x^2 > 9$ , since $16 > 9$ . So both premises (the second a conjunction of two true implications) hold for every real $x$ .

In prose: We know that $x > 5$ implies $x > 4$ , and that $x > 4$ implies $x^2 > 16$ and $x^2 > 16$ implies $x^2 > 9$ . In particular, $x > 4$ implies $x^2 > 16$ . In particular, $x^2 > 16$ implies $x^2 > 9$ . Suppose $x > 5$ . Then $x > 4$ . Hence $x^2 > 16$ . So $x^2 > 9$ . This proves that if $x > 5$ , then $x^2 > 9$ .

Marking scheme. (10 points)

2: takes the conjunctive premise apart by two $\mathrm{\wedge E}$ lines (inside or outside the box).
2: opens a box with $P$ (not $S$ ) and closes it on $S$ , a line of that box.
2: reaches $S$ inside the box of $P$ by $\mathrm{{\to}E}$ steps, each citing an implication and exactly its hypothesis, every cited line available.
1: each closing $\mathrm{{\to}I}$ cites its box as a range.
3: prose with one sentence per step, “suppose” for the assumption, and a closing sentence stating the implication.

A route that first derives $Q \to S$ in a box of $Q$ (as in Proposition 1.4.1) and then uses it in the box of $P$ earns the same points: its $\mathrm{{\to}E}$ steps in both boxes count for the third line, and its two $\mathrm{{\to}I}$ steps for the fourth.

Fatal errors (0 for the step): a box opened with the conclusion $S$ (the converse error); citing a line of the box after it has closed.

Exercise (C4: The assumptions a line depends on, used later)

Each line of a derivation depends on the premises and on the assumptions of the boxes it sits in. Take the first derivation in the proof of Proposition 1.4.2 (lines 1–7).

(a) Beside each line, write the set of line numbers of the premises and assumptions it depends on.
(b) For line 5 and for line 6, write the sequent whose premises are the statements on the lines of that set and whose conclusion is the statement of the line. Show that each is derivable, by turning the open assumptions into premises.
(c) (Challenge.) Show that, in any derivation, the set of a line cited by an $\mathrm{\wedge I}$ , $\mathrm{\wedge E}$ or $\mathrm{{\to}E}$ line is contained in the set of the citing line. Then say how the set of a $\mathrm{{\to}I}$ line compares with the set of the last line of the box it cites.

Solution.

(a) Line 1: $\{1\}$ . Line 2: $\{1, 2\}$ . Lines 3, 4 and 5: $\{1, 2, 3\}$ . Line 6: $\{1, 2\}$ . Line 7: $\{1\}$ . The premise is in every set; the assumption of line 3 only in the sets of lines 3–5, the lines of its box; the assumption of line 2 in the sets of lines 2–6.
(b) Line 5 gives $(P \wedge Q) \to R, \ P, \ Q \vdash R$ :

1 $(P \wedge Q) \to R$
2 $P$
3 $Q$
4 $P \wedge Q$ $\mathrm{{\wedge}I}$ 2, 3
5 $R$ $\mathrm{{{\to}}E}$ 1, 4

Line 6 gives $(P \wedge Q) \to R, \ P \vdash Q \to R$ ; here the box of $Q$ is kept, since line 6 lies outside it:

1 $(P \wedge Q) \to R$
2 $P$
3 $Q$ asm, for $\mathrm{{{\to}}I}$
4 $P \wedge Q$ $\mathrm{{\wedge}I}$ 2, 3
5 $R$ $\mathrm{{{\to}}E}$ 1, 4
6 $Q \to R$ $\mathrm{{{\to}}I}$ 3–5

In each, the lines down to the chosen one, with the assumptions of the boxes still open there made premises, form a derivation.
(c) A line’s set consists of the premises and the assumptions of the boxes containing it. Let line $k$ cite line $i$ by $\mathrm{\wedge I}$ , $\mathrm{\wedge E}$ or $\mathrm{{\to}E}$ . Then line $i$ is available at line $k$ , so by the scope rule of Definition 1.4.2 every box containing line $i$ also contains line $k$ . Hence the assumption of every such box is in the set of line $k$ , and the premises are in both sets: the set of $i$ is contained in the set of $k$ .

For $\mathrm{{\to}I}$ : the box’s last line is a line of the box itself, so it lies in the cited box and in the boxes around it. The $\mathrm{{\to}I}$ line lies in exactly the boxes around the cited box (the condition for a box to be available). So the set of the $\mathrm{{\to}I}$ line is the set of the box’s last line with one member removed: the line number of the box’s assumption. That is the discharge, seen as a set.

Marking scheme. (10 points)

3: all seven sets correct (the premise in every set; line 3’s assumption only in the sets of lines 3–5).
2: line 5’s sequent, with a correct derivation.
2: line 6’s sequent, with the box of $Q$ kept.
3: (c) uses the scope rule for the containment, and names the one assumption that a $\mathrm{{\to}I}$ line drops.

Fatal errors (0 for the step): putting line 3 in the set of line 6 or line 7; treating an assumption as a premise of the whole derivation.