8.4  Reading a Proof: Self-Explanation

Section 8.3 showed that a level-3 proof leaves steps unsaid by a fixed convention, and that any doubtful stretch can be expanded and checked. That presupposes a reader who notices the doubtful stretch. This section is about becoming that reader. It teaches one habit, self-explanation: for each line of a proof, say what makes it true. The habit is taught here once, on one short proof, and the rest of the book relies on it. When a later proof ends its Idea with “Before reading on: …” or “Self-explain lines 3–5”, this is the passage it means.

8.4.1. Two readers of one proof

Two people read the same proof, line by line, to the end. Both say they understood it. Asked afterwards whether it was correct, one can answer and point to the reason each line holds; the other can only repeat the proof in other words. What separates them is not intelligence or background. It is what each did at every line.

The first asked, at each line, what makes this true? and answered by pointing: to earlier lines, to a definition, to a named result, and to the rule that combines them. The second asked what does this say? and answered by restating it. Only the first answer can come out wrong, and that is exactly why it is useful. A restatement always succeeds, so it tests nothing.

To self-explain a line is to name its warrant: the earlier lines, definitions and results it comes from, and the rule that gets it from them.

The answer has the shape of a justification column in a derivation. In the derivations of Chapters 1–7 that column was printed beside every line. In level-3 prose it is gone, and self-explanation is the reader writing it back in, at level 1 or 2 of Definition 8.3.1, one line at a time.

8.4.2. The training passage

Here is a short proof. Read it once, then read the two explanations that follow.

Example (Explaining a proof, well and badly)

Claim. For every real number x>0, x+1/x≥2.

Proof. Let x>0.

  1. (x−1)2≥0.
  2. So x2−2x+1≥0.
  3. Dividing by x, x−2+1/x≥0.
  4. Hence x+1/x≥2.

Self-explain each line of the proof.

Solution. Explained well.

  • The opening. “Let x>0” opens a box for an arbitrary x with the assumption x>0: the claim is ∀x>0(x+1/x≥2), and this is its bounded ∀I. Everything below may use x>0; so far nothing has.
  • Line 1 is an instance of the school fact that the square of every real number is at least 0, at the term x−1 (a ∀E). It uses no earlier line, and in particular not x>0: it holds for every real x.
  • Line 2 follows from line 1 because (x−1)2 and x2−2x+1 are the same number, by expanding the square; one is replaced by the other (=E).
  • Line 3 follows from line 2 by dividing both sides by x. Two things need x>0 here. Dividing by x needs x≠0, and dividing both sides of an inequality by a number is guaranteed to keep its direction only when that number is positive. Both come from the assumption x>0, and this is the only place in the proof where the assumption is used. The left side becomes (x2−2x+1)/x=x−2+1/x, and the right side 0/x=0.
  • Line 4 follows from line 3 by adding 2 to both sides, which keeps any inequality. It is the claim for this x; since x was arbitrary, the claim holds for every x>0 (the closing ∀I, silent in the proof as written).

Explained badly.

  • Line 1: we start with a square, which is positive.
  • Line 2: multiply it out.
  • Line 3: now we divide by x and it still works.
  • Line 4: rearranging gives the answer.

Both explanations follow the order of the proof, and the second is not even wrong everywhere; it is shorter, and every sentence after the first describes what happened (the first we return to below). But compare what each one did with line 3. The first says why the inequality survives the division, and in saying it, finds the one place where the hypothesis x>0 earns its keep. The second says “it still works”, which is a description of the outcome, not a reason.

The difference shows as soon as the proof is wrong. Change the claim to “for every real x≠0, x+1/x≥2”, and keep all four lines. The bad explanation reads the new proof exactly as happily as the old one: we start with a square, multiply out, divide by x and it still works, rearrange. The good explanation stops at line 3. It needs “the inequality keeps its direction because x>0”, and the hypothesis now says only x≠0; for negative x, division by x reverses the inequality, and line 3 does not follow. The claim is in fact false: at x=−1, x+1/x=−2<2. A reader who explains warrants finds the gap; a reader who paraphrases cannot, because a paraphrase of a wrong step reads exactly like a paraphrase of a right one.

The bad explanation also slipped in its first line. A square is not always positive, only at least 0: (x−1)2=0 at x=1, where the claim holds with equality. Restating invites such slips, because nothing is being checked. Explaining a warrant forces the exact fact, “every square is at least 0”, because the explanation has to cite it.

So the first kind of reading does three things the second does not. It checks each step, since a warrant can fail to exist. It locates the hypotheses, since every use of a hypothesis is a warrant. And it prepares the reader to reuse the proof, since the warrants, not the restatements, are what transfer to the next problem.

8.4.3. How to explain a line

For each line, ask four questions, in this order.

  1. What kind of line is it? An assumption that opens a box (“let”, “suppose”, “choose … such that”), a line derived from earlier ones, or the closing of a box (“hence”, “so”, “since x was arbitrary”). In a derivation the annotation answers it: “asm, for →I” beside an assumption names the rule that will close its box (Section 8.1).
  2. Where does it come from? Name the earlier lines, the definitions and the results it uses. “Line 2”, “the definition of even”, “Theorem 2.1.3”, “the hypothesis x>0”. A result is named, not paraphrased.
  3. By which step? A rule of Chapters 1–7, or a piece of arithmetic that you can say in one clause (“divide both sides by x”, “expand the square”).
  4. Is it legitimate here? Is every cited line still available, inside the boxes that are open (Definition 1.4.2)? Is a chosen name fresh? Does a division have a non-zero divisor, and does an inequality keep its direction?

You do not need to write out a derivation; a phrase per line is enough, at the level of the “explained well” column above. When you cannot answer one of the four questions, you have found what to look at: either a step you do not yet understand, or a gap in the proof. Section 8.3 says what to do next: expand that stretch to level 1.

Quick check. Which of the four questions does the bad explanation of line 3 in Example (Explaining a proof, well and badly) fail to answer?

Solution. The fourth, whether the step is legitimate here: does dividing by x keep the direction of the inequality? With it the second fails too, since the warrant x>0 is never named.

Warning. Self-explanation is not re-reading, and not summarizing. Reading a proof twice more makes it familiar, not checked: familiarity is what makes the bad explanation of Example (Explaining a proof, well and badly) feel adequate. A summary (“the proof expands a square and divides by x”) is useful afterwards, but it skips exactly the warrants that matter, such as why the division by x is allowed and keeps the inequality’s direction. Self-explanation is local and backward-looking: each line, against what came before it.

Quick check. Here is a six-line proof that for real numbers x and y, if x+y>2, then x>1 or y>1.

  1. We prove the contrapositive: if it is not the case that x>1 or y>1, then x+y>2 fails.
  2. Suppose it is not the case that x>1 or y>1.
  3. Then x≤1 and y≤1.
  4. Adding these, x+y≤2.
  5. So x+y>2 fails.
  6. This proves the contrapositive, and hence the claim.

Self-explain lines 2–4.

Solution. Line 2 is an assumption: it opens the →I box for the contrapositive announced in line 1, whose hypothesis is ¬(x>1∨y>1).

Line 3 comes from line 2 in two steps. First Proposition 2.5.5 (a), ¬(P∨Q)⊢¬P∧¬Q, gives “not x>1, and not y>1”. Then the order fact that ¬(u>1) means u≤1, for every real u, turns each conjunct into the form written.

Line 4 uses both conjuncts of line 3 (∧E, twice) and the order fact that inequalities may be added: x≤1 and y≤1 give x+y≤1+y≤1+1=2.

(For the record: line 5 is the order fact x+y≤2 means ¬(x+y>2); line 6 closes the box by →I and then passes from the contrapositive to the claim by Proposition 2.5.2, a classical step.)

8.4.4. Naming the unstated fact

Section 3.3 turned a paragraph of argument into a sequent: its conclusion, its stated premises, and the unstated facts that close its gaps. A proof is read the same way, one line at a time. Often the second question, where does it come from?, has an answer the writer did not write: a fact used but not stated. Self-explaining the line means naming that fact, and the fact then turns out to be one of three things. It may be a school fact or a definition: name it. It may be an earlier result: cite it. Or it may be false, and then the line fails. Two lines that look alike:

  • “Since n2 is a multiple of 3, so is n.” The unstated fact, “if 3∣n2, then 3∣n”, is true. A careful proof proves it, by cases on the remainder of n on division by 3.
  • “Since n2 is a multiple of 4, so is n.” The unstated fact, “if 4∣n2, then 4∣n”, is false at n=2. Chapter 1 met it as a missing premise (Exercise (B5: Supply the missing premise)).

A reader who only paraphrases reads both lines alike.

Quick check. In “Since x>1, x2>x”, name the unstated fact and the hypothesis it needs.

Solution. Multiplying both sides of x>1 by x keeps the direction of the inequality because x>0; and x>0 follows from x>1>0.

8.4.5. Strategies of good readers

Self-explanation is the habit for single lines. Readers who are good at proofs also do a few things with a proof as a whole. Here are five, shown on one short proof.

Claim. For real numbers x>0 and y>0, xy≤(x+y)/2.

Proof. Let x>0 and y>0. Since x=(x)2, y=(y)2 and xy=xy, x+y−2xy=(x−y)2≥0. Hence 2xy≤x+y, and dividing by 2 gives the claim.

  1. Try it first. Before reading the proof, spend a few minutes on the claim yourself. A natural attempt squares both sides: xy≤(x+y)2/4 is 4xy≤x2+2xy+y2, that is, 0≤(x−y)2, which is true. Already you know what the difficulty is (the square root) and what your attempt rests on (that a square is at least 0).
  2. Identify the framework. Find the skeleton, level 1 of Definition 8.3.1. Here: a bounded ∀I on x and y (opened by “Let”, closed silently) with the bounds x>0, y>0, then a direct chain. There is no case split, no contradiction, and no chosen witness. Knowing that tells you where to look: every line is a computation, so every warrant is an algebraic fact.
  3. Break it into sub-proofs. The proof has one claim inside it, the displayed identity, and then a short finish. A claim inside a proof is proved once and then used, as with a lemma in Section 8.2 (“It suffices to show”). Read the claim on its own: it needs xy=xy (true for x,y≥0) and (x)2=x.
  4. Illustrate a hard line with an example. If the identity is not clear, try numbers. With x=1 and y=4: the left side is 1+4−2⋅2=1, the right side (1−2)2=1. An example checks nothing in general, but it shows what the line claims.
  5. Compare with your own attempt. Your squaring route proves the claim too, and it hides a warrant the given proof avoids: passing back from xy≤(x+y)2/4 to xy≤(x+y)/2 uses the converse of “squaring preserves order”: from a2≤b2 conclude a≤b. This holds when b≥0, because then |a|≤b; here b=(x+y)/2>0. Without that hypothesis it fails: a=1, b=−2. Comparing the two routes shows why the given proof introduces x and y: it never has to undo a squaring. The comparison also links this claim to Example (Explaining a proof, well and badly): put y=1/x, and xy=1, so the claim becomes x+1/x≥2.

The five strategies work at the level of the whole proof and self-explanation at the level of the line, and they support each other. Trying first tells you which line will be the hard one; the framework tells you which boxes are open at each line, which is what the fourth question of self-explanation needs.

8.4.6. Exercises

A. Check your understanding

Exercise (A1)

Here is a proof that if a>0, b>0 and a2=b2, then a=b.

  1. a2−b2=0. (2) (a−b)(a+b)=0. (3) a+b>0. (4) Hence a−b=0, that is, a=b.

Classify each explanation as one that justifies its line or one that paraphrases it.

  • (a) “Line 1 follows from the hypothesis a2=b2 by subtracting b2 from both sides.”
  • (b) “Line 2: then the factored form is zero as well.”
  • (c) “Line 2 is line 1 rewritten with the identity u2−v2=(u−v)(u+v), at u=a and v=b.”
  • (d) “Line 3: now we know that a+b is positive.”
  • (e) “Line 3 holds because a>0 and b>0 are hypotheses, and a sum of two positive numbers is positive.”
  • (f) “Line 4: so a−b is zero, which is what we wanted.”

Solution.

  • (a) Justifies: it names the source (the hypothesis) and the step (subtracting b2).

  • (b) Paraphrases: “is zero as well” restates line 2 without saying why the product equals the left side of line 1.

  • (c) Justifies: it names the identity and the instance.

  • (d) Paraphrases: it restates line 3 and gives no reason.

  • (e) Justifies: it names both hypotheses and the fact that combines them.

  • (f) Paraphrases: it gives no warrant. A justification would say: by line 2 a product is zero, so one of its factors is zero; line 3 says the factor a+b is not zero, being positive; so a−b=0 (Proposition 2.3.4, applied to “a+b=0 or a−b=0” and a+b≠0).

Exercise (A2: Drill)

Answer each part in a phrase. (a) and (b) ask whether an explanation justifies or paraphrases; (c) and (d) which of the four questions is at work; (e) and (f) what kind of line it is; (g)–(i) name the unstated fact; (k) locates a hypothesis; (j) and (l) are about the habits of good readers.

  • (a) A line: “Since n is even, n2 is even.” An explanation: “With n=2k, n2=2(2k2), and 2k2 is an integer.” Does it justify or paraphrase?
  • (b) A line: “x2−1=(x−1)(x+1).” An explanation: “We factor it.” Justify or paraphrase?
  • (c) Which of the four questions asks “May we divide by x−1 here?”
  • (d) Which question does the answer “this line opens a box” answer?
  • (e) What kind of line is “Choose δ>0 such that …”, and what does its derivation print beside it?
  • (f) What kind of line is “Since ε was arbitrary, …”?
  • (g) Name the unstated fact: “Since 0<a<b, a2<b2.”
  • (h) Name the unstated fact: “|x−2|<1, so x>1.”
  • (i) Name the unstated facts: “x2=9 and x>0, so x=3.”
  • (j) After three readings, a proof feels clear. Has the reader self-explained it?
  • (k) “Let x<0. Then 1/x<0.” Which hypothesis is used, and how?
  • (l) “Before reading the proof, I tried the claim myself by squaring both sides.” Which strategy is this?

Solution.

  • (a) It justifies: it names the definition of even, the witness and the algebra.

  • (b) Paraphrase. It says what happened, not which identity makes the line true (u2−v2=(u−v)(u+v) at u=x, v=1).

  • (c) The fourth: is the step legitimate here (is x−1≠0)?

  • (d) The first: what kind of line it is.

  • (e) An assumption that opens an ∃E box with a fresh name; “asm, for ∃E”.

  • (f) The closing of a ∀I box.

  • (g) Multiplying an inequality by a positive number keeps it: a⋅a<a⋅b (multiply a<b by a>0) and a⋅b<b⋅b (multiply by b>0).

  • (h) |u|<r holds exactly when −r<u<r; here −1<x−2.

  • (i) x2−9=(x−3)(x+3), and a product of real numbers is 0 only if a factor is, so x=3 or x=−3; then x>0 rules out −3 (DS).

  • (j) Not necessarily: familiarity is not a warrant checked line by line (the warning “Self-explanation is not re-reading”).

  • (k) x<0. It gives x≠0, so 1/x exists; and x⋅(1/x)=1>0, so 1/x has the sign of x.

  • (l) Try it first.

B. Practice

Exercise (B1: Self-explain a counterexample)

Here, with its lines numbered, is the half of Example (The square function on the real line) that shows f(x)=x2 is not uniformly continuous on R.

  1. By the negation of uniform continuity, with the bounds x∈R and y∈R dropped because they always hold, we must show ∃ε>0∀δ>0∃x∃y(|x−y|<δ∧|x2−y2|≥ε).
  2. Take ε=1. (3) Let δ>0 be arbitrary, and take x:=1/δ and y:=1/δ+δ/2, which depend on δ. (4) Then |x−y|=δ/2<δ, (5) and, since y>x>0, |x2−y2|=(y−x)(y+x)=δ2(2δ+δ2)=1+δ24≥1.
  3. Since δ was arbitrary, uniform continuity fails.

Self-explain each line, citing labels where a line uses an earlier result. Say at which lines δ>0 is used.

Solution. (1) The goal “not uniformly continuous” is replaced by the displayed formula: the negation of uniform continuity with no ¬ in front of a quantifier (Section 6.2’s recipe, Example (Three negations from analysis) (c)). The proof now proves that formula. (2) 1 is the witness for “there is ε>0”, and 1>0. It is written first and justified by the end. (3) δ>0 is arbitrary: what follows must work for every δ. The numbers x and y are built from δ, which is allowed because δ is already given; 1/δ exists because δ≠0. (4) y−x=δ/2>0, so |x−y|=δ/2, and δ/2<δ because δ>0. (5) Both numbers are positive and y>x, so |x2−y2|=y2−x2=(y−x)(y+x); multiplying out gives 1+δ2/4, at least 1 because a square is at least 0. (6) δ was arbitrary, so the displayed formula holds with ε=1, and uniform continuity fails. δ>0 is used in (3), in (4) twice, and in (5).

Second readingThe same lines, rule by rule

(1) A cut: the goal “f is not uniformly continuous” is replaced by the displayed formula, and the proof then proves the formula. The formula is the positive form of the negation of uniform continuity, Example (Three negations from analysis) (c), read with A=R; there the two are shown interderivable, by Proposition 6.2.3, Proposition 6.2.2 and the order fact ¬(u<ε) iff u≥ε. The direction used here is from the displayed formula to the negation. The bounds can be dropped because a bounded quantifier ∃x∈R abbreviates ∃x(x∈R∧…) (Definition 5.1.1), and over the domain R the conjunct x∈R always holds.

(2) The witness for ∃ε>0: a bounded ∃I at the term 1, with its bound 1>0. It is written first, but as a rule it is applied last: the instance it needs, the formula after ∃ε>0 with 1 for ε, is what lines (3)–(6) prove.

(3) “Let δ>0 be arbitrary” opens a bounded ∀I box flagged δ0 with the assumption δ0>0. As in Section 5.4, the prose uses the letter δ both for the flag and for the bound variable; below, δ in the arithmetic is the flag δ0. The terms 1/δ and 1/δ+δ/2 are the witnesses for ∃x and ∃y (two ∃I, applied at the end of the box). They may mention δ because δ’s box is open; the clause “which depend on δ” records this. The term 1/δ exists because δ≠0, from δ>0.

(4) Arithmetic: y−x=δ/2, which is positive since δ>0, so |x−y|=δ/2; and δ/2<δ since δ>0. This is the first conjunct.

(5) Arithmetic. Since δ>0, x=1/δ>0 and y=x+δ/2>x. Then x2<y2, so |x2−y2|=y2−x2=(y−x)(y+x), with y−x=δ/2 and y+x=2/δ+δ/2; multiplying out gives 1+δ2/4, which is at least 1 because δ2/4≥0. This is the second conjunct; with (4) it gives the conjunction (∧I), and the two ∃I of (3) then give ∃x∃y(…).

(6) The closing line of the bounded ∀I box flagged δ0 (Proposition 6.1.1). The side condition holds: the proof has no premises; the only assumption mentioning δ0 is δ0>0, the assumption of the box this line closes, and no outer box is open; and δ0 does not appear in the conclusion ∀δ>0∃x∃y(…), whose δ is a bound variable different from the flag. With (2) this proves the displayed formula, and by the cut (1) uniform continuity fails.

δ>0 is used in (3) (so that 1/δ exists), in (4) (twice) and in (5) (for y>x>0).

Exercise (B2: The unjustified line)

Here is a proof that for real numbers x<y, x3<y3.

  1. Let x<y. (2) Then y3−x3=(y−x)(y2+xy+x2). (3) Since x<y, y−x>0. (4) Also y2+xy+x2>0. (5) So y3−x3>0, as a product of two positive numbers. (6) Hence x3<y3.

Every line is true. Line 1 opens the box; of the rest, all but one are instances of a routine algebra or order fact, cited or not; one line is not an instance of any fact stated so far, and it needs an argument of its own. Self-explain the proof line by line to find it, and supply that argument as its warrant.

Solution. Line 1 opens the box, with the assumption x<y. Line 2 is the identity (y−x)(y2+xy+x2)=y3−x3, checked by multiplying out. Line 3 cites line 1 and the order fact u<v iff v−u>0. Line 5 cites lines 2, 3 and 4 and the fact that a product of two positive numbers is positive. Line 6 is line 5 rearranged by the same order fact.

Line 4 is the one without a warrant: it cites nothing, and it is not an instance of any fact stated so far. It is not obvious either, since xy can be negative. A warrant: complete the square, y2+xy+x2=(y+x2)2+3x24≥0, with equality only if x=0 and y+x/2=0, that is, only if x=y=0. Line 1 rules that out, since x<y gives x≠y. So y2+xy+x2>0. The repaired line 4 uses the hypothesis x<y a second time, which the proof as printed hides; a reader who explains only “the bracket is positive” has paraphrased line 4 and missed this.

Exercise (B3: Name the unstated facts)

Here is a proof.

Claim. For every real x≥0, x3+2≥3x.

  1. x3−3x+2=(x−1)2(x+2). (2) (x−1)2≥0. (3) x+2>0. (4) So x3−3x+2≥0, (5) that is, x3+2≥3x.
  • (a) Name the unstated fact behind each line.
  • (b) Which line uses the hypothesis x≥0, and how?
  • (c) Find the least c such that the same proof, with at most two lines reworded, proves the claim for every x≥c. Show that the claim fails at x=−3.

Solution. (a)

    1. A polynomial identity, checked by expanding: (x2−2x+1)(x+2)=x3+2x2−2x2−4x+x+2=x3−3x+2.
    1. Every square is at least 0.
    1. x≥0 gives x+2≥2>0.
    1. A product of a non-negative and a positive number is non-negative, applied to (2) and (3), then (1) substituted (=E).
    1. Adding 3x to both sides keeps the inequality.

(b) Line (3), and only there: x≥0 gives x+2≥2>0, which line (4) needs as the positive factor.

(c) c=−2. For x≥−2, line (3) becomes “x+2≥0”, and line (4) uses “a product of two non-negative numbers is non-negative”; every other line stands. Below −2 the claim is false. At x=−3: (−3)3+2=−25, while 3x=−9, and −25≥−9 fails. (For every x<−2, (x−1)2>0 and x+2<0, so the product is negative.)

Marking scheme. (10 points) - 5: (a), one per line, each naming the fact (not restating the line). - 2: (b) line (3), with how x≥0 enters. - 2: (c) c=−2, with the reworded lines (3) and (4). - 1: the failure at x=−3 computed.

Fatal errors (0 for the step): explanations that restate the lines; in (c), “the hypothesis can be dropped”.

C. Going deeper

Exercise (C1: A longer proof)

Here is a proof that a sequence has at most one limit, with its lines numbered.

Claim. If an→L and an→M, then L=M.

  1. Suppose an→L and an→M, and suppose, for a contradiction, that L≠M. (2) Let ε:=|L−M|/2. Then ε>0. (3) Choose N1∈N such that |an−L|<ε for every n≥N1, and N2∈N such that |an−M|<ε for every n≥N2. (4) Let n:=max{N1,N2}. (5) Then |L−M|≤|L−an|+|an−M|<ε+ε=|L−M|. (6) So |L−M|<|L−M|, which is impossible. (7) Hence L=M.

Self-explain each line, citing labels where a line uses an earlier result. Say where the assumption L≠M is used, and which rule closes the box it opens.

Solution (Hint 1). Line (3) applies the definition of a limit at ε. What does that need, and which line supplies it?

Solution (Hint 2). Line (5) uses one named result and two lines of (3). Which?

Solution. (1) Two openings: the →I box with the two hypotheses, and inside it a box on L≠M, that is, ¬(L=M); the goal L=M is positive, so this is an RAA box. (2) A constant, defined from L and M. It is positive because L≠M gives |L−M|>0: the one use of the assumption. (3) The definition of an→L (as in Example (Three negations from analysis) (a)) applied at ε (∀E at a term that is not the obvious one, with its bound ε>0 from (2)), then ∃E with the fresh name N1; the same for M, with a second fresh name N2 (one name for both would be (N4) of Section 8.6). (4) A constant: the larger of two natural numbers, so n≥N1 and n≥N2. (5) The triangle inequality (Example (The triangle inequality by cases)), with |L−an|=|an−L|; then the two bounds of (3) at this n (∀E at n, →E with n≥N1 and with n≥N2); then ε+ε=|L−M| by (2). (6) The clash: |L−M|<|L−M| against the fact that no number is less than itself (¬E). The line does not mention N1 or N2, so the two ∃E boxes close on it. (7) RAA: the box assumed ¬(L=M) and the line written after it is L=M. The closing of the →I box is silent. The assumption is used once, at (2), and it does work there, so the proof is not in costume; Section 8.2 proved the same claim without opening this box (Example (A sequence has at most one limit)).

Marking scheme. (10 points) - 2: (1) and (7), the two boxes and RAA as the closing rule (not ¬I). - 2: (2), ε>0 from L≠M, named as the use of the assumption. - 2: (3), the instance named, two fresh names. - 2: (5), the triangle inequality cited and both bounds applied at n≥N1,N2. - 2: (6), the clash named, and the ∃E boxes closing because ⊥ does not mention N1, N2.

Fatal errors (0 for the step): calling (7) ¬I; applying the definition at ε without its positivity.

Exercise (C2: Challenge: A proof about derivations)

Self-explain the proof of Lemma 4.8.3 in Section 4.8: for each of its five numbered steps, and for each claim in the paragraph that follows them, say what it uses and why that is legitimate. Then state the idea of the proof in two sentences.

Solution (Hint 1). Keep Definition 1.4.2 open beside you: the paragraph after the five steps checks, in turn, the premises, the scope rule for the transplanted citations, the rule schemas, the last line of each box, and the availability of what the last line cites.

Solution (Hint 2). Start with step 2. Which result supplies p∨¬p, what is substituted for its letter, and why may that line cite nothing?

Solution. Step 1. The premises of the new list are the members of Δ that D or E uses. Clause (D1) of Definition 1.4.2 places premises first, above every box, and puts no restriction on which statements they are. The conclusion will be Δ⊢ψ, so only members of Δ are taken. The premises p, ¬p of D and E are therefore left out, unless they also belong to Δ, which does no harm.

Step 2. The line p∨¬p is Proposition 2.5.3 with the atom p for the letter P, used as a derived rule (Definition 2.3.1) with no premises, so it cites nothing. This is the one classical step, through LEM.

Step 3. The box opened by p contains the non-premise lines of D with their own boxes; every citation of the premise p is redirected to the assumption, and every citation of a premise in Δ to the premise line of step 1. The two degenerate cases (the last line of D is a premise) are handled separately so that the box still ends in ψ, by repetition (R, clause (D3)) where needed.

Step 4. The same, for E with the assumption ¬p.

Step 5. The last line ψ is ∨E (Definition 1.6.1), citing the disjunction of step 2 and the two boxes, each opened by one disjunct and ending in ψ.

The verification paragraph. It checks that the list is a derivation. (i) Premises are first and in no box, so they are available everywhere. (ii) Inside each new box, a line of D cites the same lines and boxes as before, renumbered, or a premise line, or the assumption, and each of those is available by the scope rule of Definition 1.4.2: the old boxes have simply been placed inside one new box, which contains both the citing line and the cited one. (iii) Each line is still an instance of its rule’s schema, since its statement and the statements it cites are unchanged, as in the proof of Lemma 2.3.3. (iv) The last line of each new box is ψ, as a line of that box itself, which ∨E requires. (v) The disjunction and the two boxes are available at the last line, which lies in no box. So the last line is a correct ∨E, and Δ⊢ψ.

The idea in two sentences. The lemma is proof by cases on p∨¬p: excluded middle supplies the disjunction, and the two given derivations, with their premise p or ¬p turned into the assumption of a box, are the two cases of ∨E. All the work is in checking that the transplanted lines still cite only available lines.

Marking scheme. (10 points) - 2: step 2 explained: Proposition 2.5.3 as a derived rule at the atom p, citing nothing, and identified as the classical step. - 2: steps 3 and 4 explained: the redirection of citations of p (or ¬p) to the assumption and of members of Δ to the premise lines, and the degenerate cases. - 1: step 5 named as ∨E with its three citations. - 3: the verification paragraph explained against Definition 1.4.2: availability by the scope rule, schemas unchanged, each box ending in ψ as its own line. - 2: an idea in two sentences that names both the case split on p∨¬p and the transplanting of D and E into the two boxes.

Fatal errors (0 for the step): explanations that restate the steps without naming what they use; calling the case split ¬I or RAA.