8.3 Four Levels of One Proof

Sections 8.1 and 8.2 matched each rule with the phrases that carry it. A proof, though, is read and written whole. This section writes proofs several times, from a full derivation to the plain prose of a textbook, names the four levels this gives, fixes exactly which steps the last level may leave unsaid, and ends with the use that matters most to a reader working alone: when a sentence looks doubtful, rewrite it, and only it, as a skeleton, and look.

8.3.1. One short proof, four texts

Here is one proof, for every integer $n$ : if $n$ is odd, then $n^2$ is odd, written four times, starting from the version a textbook prints and zooming in.

Plain prose.

Let $n$ be odd, say $n = 2k + 1$ . Then $n^2 = 4k^2 + 4k + 1 = 2(2k^2 + 2k) + 1$ , so $n^2$ is odd.

Prose with the rules tagged.

Let $n$ be an integer [ $\mathrm{\forall I}$ ], and suppose $n$ is odd [ $\mathrm{{\to}I}$ ]; choose an integer $k$ with $n = 2k + 1$ [ $\mathrm{\exists E}$ , fresh $k$ ]. Then $n^2 = 4k^2 + 4k + 1 = 2(2k^2 + 2k) + 1$ [algebra], so $n^2$ is odd, with the witness $2k^2 + 2k$ [ $\mathrm{\exists I}$ ; then $\mathrm{\exists E}$ closes, since “ $n^2$ is odd” does not mention $k$ ]. Since $n$ was arbitrary, every odd integer has an odd square [ $\mathrm{{\to}I}$ , $\mathrm{\forall I}$ , closing].

The skeleton (domain $\mathbb{Z}$ ).

n_0

\exists k \, (n_0 = 2 \cdot k + 1)

asm, for

\mathrm{{{\to}}I}

k_0

n_0 = 2 \cdot k_0 + 1

asm, for

\mathrm{{\exists}E}

n_0 \cdot n_0 = 2 \cdot (2 \cdot k_0 \cdot k_0 + 2 \cdot k_0) + 1

arith 2

\exists j \, (n_0 \cdot n_0 = 2 \cdot j + 1)

\mathrm{{\exists}I}

\exists j \, (n_0 \cdot n_0 = 2 \cdot j + 1)

\mathrm{{\exists}E}

1, 2–4

\exists k \, (n_0 = 2 \cdot k + 1) \to \exists j \, (n_0 \cdot n_0 = 2 \cdot j + 1)

\mathrm{{{\to}}I}

1–5

\forall n \, (\exists k \, (n = 2 \cdot k + 1) \to \exists j \, (n \cdot n = 2 \cdot j + 1))

\mathrm{{\forall}I}

1–6

The full derivation. The skeleton again, with its line 3 split into two arith lines, each recording one fact: the square of $2k_0 + 1$ , then a factor $2$ taken out.

n_0

\exists k \, (n_0 = 2 \cdot k + 1)

asm, for

\mathrm{{{\to}}I}

k_0

n_0 = 2 \cdot k_0 + 1

asm, for

\mathrm{{\exists}E}

n_0 \cdot n_0 = 4 \cdot k_0 \cdot k_0 + 4 \cdot k_0 + 1

arith 2

n_0 \cdot n_0 = 2 \cdot (2 \cdot k_0 \cdot k_0 + 2 \cdot k_0) + 1

arith 3

\exists j \, (n_0 \cdot n_0 = 2 \cdot j + 1)

\mathrm{{\exists}I}

\exists j \, (n_0 \cdot n_0 = 2 \cdot j + 1)

\mathrm{{\exists}E}

1, 2–5

\exists k \, (n_0 = 2 \cdot k + 1) \to \exists j \, (n_0 \cdot n_0 = 2 \cdot j + 1)

\mathrm{{{\to}}I}

1–6

\forall n \, (\exists k \, (n = 2 \cdot k + 1) \to \exists j \, (n \cdot n = 2 \cdot j + 1))

\mathrm{{\forall}I}

1–7

Four texts, one proof. Each keeps the box of $n$ , the assumption that $n$ is odd, the choice of $k$ and the computation; they differ in how much of the routine work the reader is trusted to restore.

A derivation, a skeleton and a paragraph are the same proof; they differ in what the reader is trusted to restore.

Quick check. In the plain prose, which words stand for line 2 of the skeleton, and which skeleton lines have no words at all?

Solution. “Say $n = 2k + 1$ ” is line 2, the opening of the $\mathrm{\exists E}$ box with the fresh name $k$ . Lines 5, 6 and 7, the closings of the three boxes, have no words. “So $n^2$ is odd” is line 4, the $\mathrm{\exists I}$ .

Sections 2.2 and 6.4 already printed proofs twice, once as a derivation and once as a paragraph. The four texts you have just read are the four levels of the next definition.

Definition 8.3.1 (Levels of Proof)

A proof can be written at four levels.

Level 0, the full derivation. A derivation in the sense of Definition 1.4.2, with the rules of Chapters 1, 2 and 5: every line is a premise, an assumption, or one rule applied to available lines. A derived rule used as one line (Definition 2.3.1), such as the bounded rules of Proposition 6.1.1, counts as one rule. Facts about numbers enter as premises, or as lines justified “arith”, each of which records one such fact applied to the lines it cites.
Level 1, the skeleton. The boxes and the logical lines only: every assumption, every flagged name, every line that opens or closes a box, with the rule that closes it, and every line that such a closing line cites. Each stretch of mathematics between them is compressed into one line, justified “arith”, “by def”, or by a cited result; a stretch of routine logical steps inside one box is compressed into one line justified by the names of its rules in order, such as “ $\mathrm{\forall E}$ , $\mathrm{\exists I}$ ”.
Level 2, annotated prose. Sentences, each tagged in brackets with the rule or rules it carries, such as [ $\mathrm{\forall I}$ ] or [ $\mathrm{\exists E}$ ].
Level 3, plain prose. Sentences without tags, in which some steps are left unsaid. Which steps may be left unsaid is fixed by the convention that follows, not by the writer.

In words: level 0 hides no logic. Every line other than an arith line can be checked mechanically against the schema of its rule, and each arith line records one fact about numbers that can be checked by hand. Level 1 keeps the logical architecture and lets the arithmetic run in blocks. Level 2 is level 1 turned into sentences, with the architecture still labeled. Level 3 removes the labels and some of the lines, following a fixed convention.

Second readingLevels already on the page, and a skeleton missing a box

The levels are already on the page in earlier chapters. The derivation in Section 6.4 is level 0. The paragraph after Theorem 2.2.1, with its tags $[\mathrm{{\to}E}]$ , $[\mathrm{\wedge I}]$ , $[\mathrm{\neg E}]$ , $[\mathrm{\neg I}]$ , is level 2 for the rules Chapter 2 had; its quantifier steps carry no tags. The derivation printed below that paragraph is not quite level 0, and the reason is instructive: it fixes $r$ , $p$ and $q$ in advance and leaves out the two quantifier steps, choosing $p$ , $q$ (and later $m$ ) and passing from one $r$ to every $r$ , because Chapter 2 had no rules for them yet. Section 2.2 says so in the paragraph after the derivation. With Chapter 5’s rules those steps can be written. The example of the square root of two below writes the choices of $p$ and $q$ and the step to every $r$ ; the choice of $m$ stays inside the arithmetic fact of line 15 of its level-0 derivation (in the fold “Level 0 of the square root of two”), since evenness is treated there as a single predicate $E$ .

A non-example, by one change: take a level-1 skeleton and delete one of its boxes, say the box in which a name $N_0$ is chosen, keeping the lines inside. The result is not a shorter skeleton. It is a list in which $N_0$ appears from nowhere, and no reader can tell whether it was chosen, given, or assumed. A skeleton may compress the work inside a box; it may not compress the boxes.

Why four levels and not two? Because each serves a task. Level 0 is for settling a doubt completely: nothing in it is taken on trust. Level 1 is for planning a proof and for reading one: it is what you write on scratch paper before the first sentence (Section 8.5 turns this into a procedure), and what you reconstruct from a textbook when a proof will not come clear (Section 8.4). Level 2 is for learning, which is why this volume uses it. Level 3 is what mathematicians read and write.

Warning. A skeleton is not a finished proof. A level-1 text with lines such as “ $\left| x_0 - y \right| < \delta_0 \to \left| f(x_0) - f(y) \right| < \varepsilon_0$ , arith” is a plan: it says that a computation goes there, and it can hide a computation that does not work. For $f(x) = x^2$ on $\mathbb{R}$ , a skeleton of “ $f$ is uniformly continuous” with one line “arith” at that point looks exactly like a correct skeleton for $f(x) = 3x + 1$ , where $\delta = \varepsilon/3$ works because $\left| (3x+1)-(3y+1) \right| = 3\left| x-y \right|$ ; the claim is false for the first function (Example (The square function on the real line)), and only writing out the arithmetic shows where it fails. Expand every “arith” line before calling the proof done.

8.3.2. Which steps may be silent

Section 8.1 stated the principle: a step may go unsaid when its result is forced by the lines around it; every choice, assumption and citation is spoken. The most common cases:

The step	Silent?	Why
the closing line of $\mathrm{{\to}I}$ , $\mathrm{\forall I}$ , $\mathrm{\vee E}$ or $\mathrm{\exists E}$ (not of $\mathrm{\neg I}$ , $\mathrm{RAA}$ or $\mathrm{{\leftrightarrow}I}$ ): “since $x$ was arbitrary”, “in either case”, “hence if $P$ then $Q$ ”	may be	the box decides it
$\mathrm{\wedge E}$ ; $\mathrm{\vee I}$ ; repeating a line already shown	may be	the next sentence shows which part or form was used
$\mathrm{\forall E}$ at the name in sight; $\mathrm{{=}E}$ inside a chain	may be	the sentence that uses it forces it
opening a box: “let”, “suppose”, “choose …” with a new name	never	it creates a name or an assumption
a witness, with what it depends on; a case split, with why the cases cover everything	never	it is a choice
a citation of a hypothesis or a result; the clash of $\mathrm{\neg E}$ ; the conclusion of $\mathrm{\neg I}$ or $\mathrm{RAA}$	never	the reader cannot guess what licensed it

The official list, which the rest of the book checks written proofs against, is the next definition. The table gives its most common entries; the definition gives all of them.

Definition 8.3.2 (Silent Steps)

In level-3 prose the following steps may be silent, that is, left unwritten:

$\mathrm{\wedge I}$ when both conjuncts are displayed, and $\mathrm{\wedge E}$ ;
$\mathrm{R}$ ;
$\mathrm{\vee I}$ ;
$\mathrm{\bot E}$ , once the contradiction or the empty case has been stated;
the name of $\mathrm{DS}$ (not the fact it uses);
the exchange of the two members of a disjunction or of a conjunction (Example (First derivations with “or”), Proposition 1.2.1), made only to match the schema of a rule, with no citation;
$\mathrm{{\leftrightarrow}E}$ with a definition (“that is”, “by definition”, or nothing);
$\mathrm{\forall E}$ at the obvious term;
$\mathrm{{\to}E}$ whose implication is a line already in the proof that is neither a hypothesis of the statement, nor a cited result, nor an instance of one (for instance, an instance of the property of a chosen name), when its antecedent is displayed or has just been assumed;
$\mathrm{{=}I}$ and $\mathrm{{=}E}$ inside a chain of equalities or inequalities;
the phrase “it suffices to show”, when the claim of the cut is displayed and then used;
the closing lines of $\mathrm{{\to}I}$ (“hence if $P$ then $Q$ ”), of $\mathrm{\forall I}$ (“since $x$ was arbitrary”), of $\mathrm{\vee E}$ (“in either case”) and of $\mathrm{\exists E}$ (the conclusion repeated outside the box of the chosen name).

The following are never silent:

the openings of $\mathrm{{\to}I}$ , $\mathrm{\neg I}$ , $\mathrm{RAA}$ and $\mathrm{\forall I}$ , and of $\mathrm{\exists E}$ with a fresh name;
the conclusions of $\mathrm{\neg I}$ and of $\mathrm{RAA}$ (“hence $\neg P$ ”, “hence $P$ ”);
a $\mathrm{\neg\neg E}$ or $\mathrm{LEM}$ step, written as an explicit case split or as an explicit removal of a double negation (Proposition 2.5.1 (b); “ $P$ must hold, since …”), with the flag of Section 8.7 when the step is genuinely non-constructive;
the case split of $\mathrm{\vee E}$ , with the reason the cases exhaust;
the clash of $\mathrm{\neg E}$ : both members of the clashing pair are named;
the witness of $\mathrm{\exists I}$ , with what it depends on;
an instance of $\mathrm{\forall E}$ at a term that is not the obvious one;
every citation, and so every $\mathrm{{\to}E}$ whose implication is a hypothesis of the statement or a cited result, or an instance of one;
both directions of $\mathrm{{\leftrightarrow}I}$ , and both halves of an $\exists!$ proof;
the base case and the step of an induction, with the induction hypothesis stated;
the announcement of a contrapositive;
the negated form, after De Morgan (Proposition 2.5.5) or a quantifier negation (Proposition 6.2.1, Proposition 6.2.3);
the claim of a cut;
a “without loss of generality”, together with the symmetry that licenses it.

The eighth and ninth items of the first list, for instance, say this: after “choose $N$ such that $\left| a_n - L \right| < \varepsilon$ for every $n \ge N$ ”, applying that line to a particular $n \ge N$ needs no comment.

Silent steps and truth tables. Section 4.8 named the step that a truth table licenses, TAUT (Definition 4.8.1). Section 6.3 let it act on the propositional skeleton of a first-order line, where every atomic and every quantified part counts as a letter (Definition 6.3.1, Proposition 6.3.1). Most items of the first list are TAUT steps: $\mathrm{\wedge I}$ with both conjuncts displayed, $\mathrm{\wedge E}$ , $\mathrm{R}$ , $\mathrm{\vee I}$ , $\mathrm{\bot E}$ once the contradiction is stated, $\mathrm{DS}$ , the exchange of the members of a disjunction or conjunction, $\mathrm{{\leftrightarrow}E}$ with a definition, and $\mathrm{{\to}E}$ on a line of the proof. A reader can check each of them by a truth table on the skeleton. The quantifier and equality items, $\mathrm{\forall E}$ at the obvious term and $\mathrm{{=}I}$ and $\mathrm{{=}E}$ inside chains, are not TAUT steps: they are silent because the sentence that uses them forces them. TAUT never licenses a first-order law. On the skeleton, $\forall x\, \forall y\, R(x, y)$ and $\forall y\, \forall x\, R(x, y)$ are two different letters, so passing from one to the other is a derivation with the quantifier rules, not a TAUT step. From Section 6.3 on, a level-1 line that compresses propositional steps inside one box may cite TAUT with its lines, in place of the names of its rules.

Warning. Level 3 is not level 0 with steps missing at random. A proof that skips the reason a case split is exhaustive, or chooses $\delta$ without saying what it depends on, or uses a lemma without naming it, is not “written at level 3”: it has a gap, because those steps are in the never-silent list. Conversely, a proof that omits “since $\varepsilon$ was arbitrary” has no gap. When you judge whether a written proof is complete, judge it against Definition 8.3.2, not against your sense of what is obvious.

Second readingThe two lists against the principle, with an example

Read the two lists against the principle. Everything in the first list is forced. $\mathrm{\wedge E}$ has one premise and two possible conclusions, and the next sentence shows which was used. The closing line of a box is determined by the box. $\mathrm{\forall E}$ at the obvious term $x$ , when $x$ is the name in sight, is forced by the sentence that uses it. Everything in the second list carries information that the surrounding lines do not determine. Which name is chosen, and that it is fresh; which witness, and what it depends on; which cases, and why they are all the cases; which result is cited. A reader who meets “Then $p$ is even” with no citation has to guess what licensed it, and a guess is not a check.

A small example. In “since $x \in (0, 1)$ , in particular $x > 0$ ”, the step from the conjunction “ $0 < x$ and $x < 1$ ” to its first conjunct is $\mathrm{\wedge E}$ , and the unwinding of $x \in (0, 1)$ into that conjunction is $\mathrm{{\leftrightarrow}E}$ with the definition of an interval. Both may be silent, and here the writer kept the phrase “in particular” anyway, which is allowed: the convention says what may be omitted, never what must be. On the other side, “suppose $r^2 = 2$ ” can never be omitted from the proof of Theorem 2.2.1: without it, the reader does not know that a box has opened, and the final “ $r^2 \ne 2$ ” has no visible source.

Quick check. At level 3, may each of these be left out: (i) “since $\varepsilon$ was arbitrary”; (ii) “choose $\delta > 0$ (depending on $\varepsilon$ ) such that …”; (iii) “by the triangle inequality”?

Solution.

(i) Yes: it is the closing of $\mathrm{\forall I}$ . (ii) No: it is an $\mathrm{\exists E}$ with a fresh name, and the dependence of a witness. (iii) No: it is a citation.

8.3.3. The irrationality of the square root of two, four times

The first example is the proof of Theorem 2.2.1, now with every quantifier step written. It uses the fact that Section 2.2 calls (L): every rational number is $p/q$ for integers $p$ , $q$ with $q \ne 0$ , not both even. Write $E(x)$ for “ $x$ is even”. The proof uses only two clauses of (L), and in a convenient form: $r = p/q$ with $q \ne 0$ gives $p = r \cdot q$ , which avoids division; and “not both even” is $\neg(E(p) \wedge E(q))$ . The clause $q \ne 0$ is then not needed at all, since $q = 0$ would force $p = 0$ , and both would be even. It also uses Theorem 2.1.3, which we write as the formula $\forall n \in \mathbb{Z} \; (E(n \cdot n) \to E(n))$ . To keep the lines short, write $L(r, p, q)$ for $p = r \cdot q \wedge \neg(E(p) \wedge E(q))$ .

Example (The irrationality of the square root of two at four levels)

Write the proof of Theorem 2.2.1, that no rational number has square $2$ , at levels 0, 1, 2 and 3 of Definition 8.3.1, and match the levels line by line.

Idea. The move this example shows in full is skeleton first: before any arithmetic, write the first and the last line of every box. The goal $\forall r \in \mathbb{Q} \; \neg(r \cdot r = 2)$ dictates the outer box ( $\mathrm{\forall I}$ , “let $r \in \mathbb{Q}$ ”) and the next one ( $\mathrm{\neg I}$ , “suppose $r^2 = 2$ ”, ending in $\bot$ ). Inside, (L) instantiated at $r_0$ is an existential, so its $\mathrm{\exists E}$ boxes open at once, with fresh names $p_0$ , $q_0$ , and they too end in $\bot$ . Only then is there something to compute: the arithmetic fills the innermost box, and it has a target, the clash with “not both even”. Sections 8.5 and 8.6 come back to this move twice, with parts of the proof left blank.

Before reading on: the level-3 proof below has four sentences. Which lines of the level-1 skeleton does its second sentence, “By (L), write $r = p/q$ …”, stand for?

Solution. Level 3.

Let $r$ be rational, and suppose $r^2 = 2$ . By (L), write $r = p/q$ with integers $p$ , $q$ , not both even. Then $p^2 = 2q^2$ , so $p^2$ is even, and $p$ is even by Theorem 2.1.3; writing $p = 2m$ gives $q^2 = 2m^2$ , so $q$ is even by the same theorem. Thus $p$ and $q$ are both even, a contradiction; hence $r^2 \ne 2$ .

Level 2.

Let $r \in \mathbb{Q}$ [ $\mathrm{\forall I}$ : the box of $r_0$ ], and suppose $r^2 = 2$ [assumption for $\mathrm{\neg I}$ ]. By (L), there are integers $p$ and $q$ with $p = rq$ , not both even; choose such $p$ and $q$ [ $\mathrm{\forall E}$ at $r$ , then $\mathrm{\exists E}$ twice, with fresh names]. Then $p^2 = r^2 q^2 = 2q^2$ [arith], so $p^2$ is even [arith], and by Theorem 2.1.3 $p$ is even [ $\mathrm{\forall E}$ at $p$ , $\mathrm{{\to}E}$ ]. Writing $p = 2m$ , we get $4m^2 = 2q^2$ , so $q^2 = 2m^2$ is even [arith], and by the same theorem $q$ is even [ $\mathrm{\forall E}$ at $q$ , $\mathrm{{\to}E}$ ]. So $p$ and $q$ are both even [ $\mathrm{\wedge I}$ ], while they were chosen not both even: a contradiction [ $\mathrm{\neg E}$ ; then $\mathrm{\exists E}$ twice, since $\bot$ mentions neither $p$ nor $q$ ]. Hence $r^2 \ne 2$ [ $\mathrm{\neg I}$ ]. Since $r$ was arbitrary, no rational number has square $2$ [ $\mathrm{\forall I}$ ].

Level 1. Level 1 keeps every box, every assumption and every closing line, and compresses the work between them into three lines.

\forall r \in \mathbb{Q} \; \exists p \in \mathbb{Z} \; \exists q \in \mathbb{Z} \; L(r, p, q)

r_0

r_0 \in \mathbb{Q}

asm, for

\mathrm{{\forall}I}

r_0 \cdot r_0 = 2

asm, for

\mathrm{{\neg}I}

\exists p \in \mathbb{Z} \; \exists q \in \mathbb{Z} \; L(r_0, p, q)

\mathrm{{\forall}E}

1, 2

p_0

p_0 \in \mathbb{Z}

asm, for

\mathrm{{\exists}E}

\exists q \in \mathbb{Z} \; L(r_0, p_0, q)

asm, for

\mathrm{{\exists}E}

q_0

q_0 \in \mathbb{Z}

asm, for

\mathrm{{\exists}E}

L(r_0, p_0, q_0)

asm, for

\mathrm{{\exists}E}

E(p_0)

\wedge

E; arith; lemma 3, 5, 7, 8

E(q_0)

arith; lemma 3, 5, 7, 8, 9

\bot

\wedge

\wedge

\neg

E 8, 9, 10

\bot

\mathrm{{\exists}E}

6, 7–11

\bot

\mathrm{{\exists}E}

4, 5–12

\neg(r_0 \cdot r_0 = 2)

\mathrm{{\neg}I}

3–13

\forall r \in \mathbb{Q} \; \neg(r \cdot r = 2)

\mathrm{{\forall}I}

2–14

Line 9 takes the first conjunct out of $L(r_0, p_0, q_0)$ , and line 11 the second.

The answer to the prompt: “By (L), write $r = p/q$ with integers $p$ , $q$ , not both even” stands for line 4 ( $\mathrm{\forall E}$ of premise 1 at $r_0$ ) and for the openings of the two $\mathrm{\exists E}$ boxes, lines 5–8. It also displays the conjunct $r = p/q$ on its own, so the $\mathrm{\wedge E}$ inside line 9 that takes it out has nothing left to say.

Second readingLevel 0 of the square root of two

Level 0. Premise 1 is (L) in the form above, premise 2 is Theorem 2.1.3. The derivation has 24 lines.

\forall r \in \mathbb{Q} \; \exists p \in \mathbb{Z} \; \exists q \in \mathbb{Z} \; (p = r \cdot q \wedge \neg(E(p) \wedge E(q)))

\forall n \in \mathbb{Z} \; (E(n \cdot n) \to E(n))

r_0

r_0 \in \mathbb{Q}

asm, for

\mathrm{{\forall}I}

r_0 \cdot r_0 = 2

asm, for

\mathrm{{\neg}I}

\exists p \in \mathbb{Z} \; \exists q \in \mathbb{Z} \; (p = r_0 \cdot q \wedge \neg(E(p) \wedge E(q)))

\mathrm{{\forall}E}

1, 3

p_0

p_0 \in \mathbb{Z}

asm, for

\mathrm{{\exists}E}

\exists q \in \mathbb{Z} \; (p_0 = r_0 \cdot q \wedge \neg(E(p_0) \wedge E(q)))

asm, for

\mathrm{{\exists}E}

q_0

q_0 \in \mathbb{Z}

asm, for

\mathrm{{\exists}E}

p_0 = r_0 \cdot q_0 \wedge \neg(E(p_0) \wedge E(q_0))

asm, for

\mathrm{{\exists}E}

p_0 = r_0 \cdot q_0

\mathrm{{\wedge}E}

p_0 \cdot p_0 = 2 \cdot (q_0 \cdot q_0)

arith 4, 10

E(p_0 \cdot p_0)

arith 8, 11

E(p_0 \cdot p_0) \to E(p_0)

\mathrm{{\forall}E}

2, 6

E(p_0)

\mathrm{{{\to}}E}

13, 12

E(q_0 \cdot q_0)

arith 6, 8, 11, 14

E(q_0 \cdot q_0) \to E(q_0)

\mathrm{{\forall}E}

2, 8

E(q_0)

\mathrm{{{\to}}E}

16, 15

E(p_0) \wedge E(q_0)

\mathrm{{\wedge}I}

14, 17

\neg(E(p_0) \wedge E(q_0))

\mathrm{{\wedge}E}

\bot

\mathrm{{\neg}E}

18, 19

\bot

\mathrm{{\exists}E}

7, 8–20

\bot

\mathrm{{\exists}E}

5, 6–21

\neg(r_0 \cdot r_0 = 2)

\mathrm{{\neg}I}

4–22

\forall r \in \mathbb{Q} \; \neg(r \cdot r = 2)

\mathrm{{\forall}I}

3–23

The three “arith” lines are facts about integers, each checkable by hand. Line 11: $p_0 \cdot p_0 = (r_0 q_0)(r_0 q_0) = (r_0 \cdot r_0)(q_0 \cdot q_0) = 2 \cdot (q_0 \cdot q_0)$ , by lines 10 and 4. Line 12: $p_0 \cdot p_0$ is $2$ times the integer $q_0 \cdot q_0$ , so it is even. Line 15: by line 14, $p_0 = 2m$ for an integer $m$ ; then line 11 reads $4m^2 = 2 q_0^2$ , so $q_0^2 = 2m^2$ is even. The side conditions at the flagged lines hold: at line 21 the flag $q_0$ is not in $\bot$ , in line 7, in a premise, or in the assumptions still open (lines 3, 4, 6, 7); at line 22 the flag $p_0$ is not in $\bot$ , in line 5, in a premise, or in lines 3 and 4; at line 24 the flag $r_0$ is in no premise and not in line 24.

Level-1 line 9 is level-0 lines 10–14; line 10 is lines 15–17; line 11 is lines 18–20. Premise 2 is not a line of level 1; it is cited as “lemma”. Every other line of level 1 is a line of level 0, renumbered.

At level 0, “By (L), write $r = p/q$ with integers $p$ , $q$ , not both even” stands for line 5 ( $\mathrm{\forall E}$ of premise 1 at $r_0$ ) and for the openings of the two $\mathrm{\exists E}$ boxes, lines 6–9. It also displays the conjunct, in the form $r = p/q$ , on its own, so the $\mathrm{\wedge E}$ of line 10 that extracts it has nothing left to say and can be silent.

A check at level 0.

Quick check. Which lines of the level-0 derivation in Example (The irrationality of the square root of two at four levels) have no counterpart in the level-3 text, and which item of Definition 8.3.2 lets each go?

Solution. Eight lines. Line 5 is $\mathrm{\forall E}$ of premise 1 at the obvious term $r_0$ , the name in sight; “By (L)” cites premise 1, and the instance is not written. Lines 10 and 19 are $\mathrm{\wedge E}$ . Lines 13 and 16 are $\mathrm{\forall E}$ of the lemma at the obvious terms $p_0$ and $q_0$ ; the citations “by Theorem 2.1.3” and “by the same theorem” remain, and they are the $\mathrm{{\to}E}$ lines 14 and 17. Lines 21 and 22 are the closing lines of the two $\mathrm{\exists E}$ boxes. Line 24 is the closing line of $\mathrm{\forall I}$ : level 3 never says “since $r$ was arbitrary”. Every other line has a phrase: lines 1 and 2, the premises, are the citations “By (L)” and “by Theorem 2.1.3”; lines 3, 4, 6–9 the openings; lines 11, 12, 15 the arithmetic; lines 14, 17 the citations; lines 18 and 20 the clash, “both even, a contradiction”, which names the pair through “not both even” two sentences earlier; and line 23, “hence $r^2 \ne 2$ ”, the conclusion of $\mathrm{\neg I}$ , which is never silent.

Look at what the four texts share. Every level has the box of $r$ , the box of the assumption $r^2 = 2$ , the choice of $p$ and $q$ , two uses of the lemma, and a contradiction followed by “hence $r^2 \ne 2$ ”. That common part is the proof; the rest is how much of the routine work each reader is trusted to do. The skeleton is the place where you can see it most clearly: fifteen lines, of which only lines 9 and 10 carry the mathematics; every other line is a decision about logic.

Quick check. Which lines of the level-1 skeleton in Example (The irrationality of the square root of two at four levels) have no counterpart in the level-3 text, and which item of Definition 8.3.2 lets each go?

Solution. Four lines. Line 4 is $\mathrm{\forall E}$ of premise 1 at the obvious term $r_0$ , the name in sight; “By (L)” cites premise 1, and the instance is not written. Lines 12 and 13 are the closing lines of the two $\mathrm{\exists E}$ boxes. Line 15 is the closing line of $\mathrm{\forall I}$ : level 3 never says “since $r$ was arbitrary”. Every other line has a phrase: line 1 is “By (L)”; lines 2, 3 and 5–8 the openings; lines 9 and 10 the computations with their citations of Theorem 2.1.3; line 11 the clash, “both even, a contradiction”; and line 14, “hence $r^2 \ne 2$ ”, the conclusion of $\mathrm{\neg I}$ , which is never silent.

8.3.4. Uniform continuity, twice

The second example has no arithmetic at all. That makes it a good test of the levels: what is left when there is nothing to compress?

Example (Uniformly continuous implies continuous, at four levels)

Write the proof of Example (Uniformly continuous implies continuous), that a function uniformly continuous on $A$ is continuous at every point of $A$ , at levels 1 and 3, and say where each level records what $\delta$ depends on.

Solution. Level 1. Every line of the full derivation of Example (Uniformly continuous implies continuous) other than the premise opens or closes a box, or is cited by a closing line, except one stretch inside the box of $\delta_0$ , which becomes line 7.

\forall \varepsilon > 0 \; \exists \delta > 0 \; \forall x \in A \; \forall y \in A \; (\left| x - y \right| < \delta \to \left| f(x) - f(y) \right| < \varepsilon)

x_0

x_0 \in A

asm, for

\mathrm{{\forall}I}

\varepsilon_0

\varepsilon_0 > 0

asm, for

\mathrm{{\forall}I}

\exists \delta > 0 \; \forall x \in A \; \forall y \in A \; (\left| x - y \right| < \delta \to \left| f(x) - f(y) \right| < \varepsilon_0)

\mathrm{{\forall}E}

1, 3

\delta_0

\delta_0 > 0

asm, for

\mathrm{{\exists}E}

\forall x \in A \; \forall y \in A \; (\left| x - y \right| < \delta_0 \to \left| f(x) - f(y) \right| < \varepsilon_0)

asm, for

\mathrm{{\exists}E}

\exists \delta > 0 \; \forall y \in A \; (\left| x_0 - y \right| < \delta \to \left| f(x_0) - f(y) \right| < \varepsilon_0)

\forall

\exists

I 2, 5, 6

\exists \delta > 0 \; \forall y \in A \; (\left| x_0 - y \right| < \delta \to \left| f(x_0) - f(y) \right| < \varepsilon_0)

\mathrm{{\exists}E}

4, 5–7

\forall \varepsilon > 0 \; \exists \delta > 0 \; \forall y \in A \; (\left| x_0 - y \right| < \delta \to \left| f(x_0) - f(y) \right| < \varepsilon)

\mathrm{{\forall}I}

3–8

\forall x \in A \; \forall \varepsilon > 0 \; \exists \delta > 0 \; \forall y \in A \; (\left| x - y \right| < \delta \to \left| f(x) - f(y) \right| < \varepsilon)

\mathrm{{\forall}I}

2–9

Level 3.

Let $x \in A$ and $\varepsilon > 0$ . By uniform continuity, choose $\delta > 0$ (depending on $\varepsilon$ only) such that $\left| f(u) - f(v) \right| < \varepsilon$ for all $u, v \in A$ with $\left| u - v \right| < \delta$ . In particular $\left| f(x) - f(y) \right| < \varepsilon$ for every $y \in A$ with $\left| x - y \right| < \delta$ , so this $\delta$ works for $x$ and $\varepsilon$ .

Where the dependence of $\delta$ is recorded. At level 1, in two places: the box of $\delta_0$ lies inside the boxes of $x_0$ and $\varepsilon_0$ , so $\delta_0$ may depend on both; and the line it comes from, line 4, mentions $\varepsilon_0$ and not $x_0$ , so it does depend only on $\varepsilon_0$ (Section 6.4). At level 3 it is the parenthesis “(depending on $\varepsilon$ only)”, and nothing else: the parenthesis is the whole of the box structure that survives. Section 8.2’s picture draws the same record.

Second readingLevels 0 and 2 of the same proof

Level 0 is the derivation of Example (Uniformly continuous implies continuous), copied here with the same line numbers. Line 1 is uniform continuity (UC), line 11 is continuity at every point (C).

\forall \varepsilon > 0 \; \exists \delta > 0 \; \forall x \in A \; \forall y \in A \; (\left| x - y \right| < \delta \to \left| f(x) - f(y) \right| < \varepsilon)

x_0

x_0 \in A

asm, for

\mathrm{{\forall}I}

\varepsilon_0

\varepsilon_0 > 0

asm, for

\mathrm{{\forall}I}

\exists \delta > 0 \; \forall x \in A \; \forall y \in A \; (\left| x - y \right| < \delta \to \left| f(x) - f(y) \right| < \varepsilon_0)

\mathrm{{\forall}E}

1, 3

\delta_0

\delta_0 > 0

asm, for

\mathrm{{\exists}E}

\forall x \in A \; \forall y \in A \; (\left| x - y \right| < \delta_0 \to \left| f(x) - f(y) \right| < \varepsilon_0)

asm, for

\mathrm{{\exists}E}

\forall y \in A \; (\left| x_0 - y \right| < \delta_0 \to \left| f(x_0) - f(y) \right| < \varepsilon_0)

\mathrm{{\forall}E}

6, 2

\exists \delta > 0 \; \forall y \in A \; (\left| x_0 - y \right| < \delta \to \left| f(x_0) - f(y) \right| < \varepsilon_0)

\mathrm{{\exists}I}

5, 7

\exists \delta > 0 \; \forall y \in A \; (\left| x_0 - y \right| < \delta \to \left| f(x_0) - f(y) \right| < \varepsilon_0)

\mathrm{{\exists}E}

4, 5–8

\forall \varepsilon > 0 \; \exists \delta > 0 \; \forall y \in A \; (\left| x_0 - y \right| < \delta \to \left| f(x_0) - f(y) \right| < \varepsilon)

\mathrm{{\forall}I}

3–9

\forall x \in A \; \forall \varepsilon > 0 \; \exists \delta > 0 \; \forall y \in A \; (\left| x - y \right| < \delta \to \left| f(x) - f(y) \right| < \varepsilon)

\mathrm{{\forall}I}

2–10

Level 1. Every line of level 0 other than the premise opens or closes a box, or is cited by a closing line, except line 7: lines 7 and 8, which specialize the chosen $\delta_0$ to the point $x_0$ and repackage the result, are the one stretch of work inside a box.

Level 2.

Let $x \in A$ [ $\mathrm{\forall I}$ ] and let $\varepsilon > 0$ [ $\mathrm{\forall I}$ ]. By uniform continuity, applied at $\varepsilon$ [ $\mathrm{\forall E}$ ], there is $\delta > 0$ such that $\left| u - v \right| < \delta$ implies $\left| f(u) - f(v) \right| < \varepsilon$ for all $u, v \in A$ ; choose such a $\delta$ , which depends on $\varepsilon$ only [ $\mathrm{\exists E}$ ]. Taking $u = x$ [ $\mathrm{\forall E}$ ], every $y \in A$ with $\left| x - y \right| < \delta$ has $\left| f(x) - f(y) \right| < \varepsilon$ . So this $\delta$ works for $x$ and $\varepsilon$ [ $\mathrm{\exists I}$ ; then $\mathrm{\exists E}$ closes, since “some $\delta$ works” does not mention the chosen one]. Since $\varepsilon$ and $x$ were arbitrary, $f$ is continuous at every point of $A$ [ $\mathrm{\forall I}$ twice].

As in Section 6.4, the prose renames the bound variables of UC to $u$ , $v$ , so that $x$ can name the fixed point.

Where the dependence of $\delta$ is recorded. At level 0, in two places: the box of $\delta_0$ lies inside the boxes of $x_0$ and $\varepsilon_0$ , so $\delta_0$ may depend on both; and the line it comes from, line 4, mentions $\varepsilon_0$ and not $x_0$ , so it does depend only on $\varepsilon_0$ (Section 6.4). At level 1 the record is the same, lines 3 to 5 being unchanged. At level 2 it is the clause “which depends on $\varepsilon$ only”, placed at the $\mathrm{\exists E}$ tag, after the $\mathrm{\forall E}$ at $\varepsilon$ that produced it. At level 3 it is the parenthesis “(depending on $\varepsilon$ only)”, and nothing else: the parenthesis is the whole of the box structure that survives.

Here the gap between level 0 and level 1 is one line, because there is no arithmetic to compress.

From level 1 to level 3, ten lines become three sentences. What the level-3 text keeps is exactly the never-silent part of Definition 8.3.2: the openings of the two $\mathrm{\forall I}$ boxes (“let $x \in A$ and $\varepsilon > 0$ ”), the citation and the choice with its fresh name (“by uniform continuity, choose $\delta$ ”), the dependence of the witness, and the witness itself (“this $\delta$ works”). The $\mathrm{\forall E}$ at $u = x$ , inside line 7, is the obvious instance and becomes “in particular”. The $\mathrm{\exists E}$ closing line 8 and the two $\mathrm{\forall I}$ closing lines 9 and 10 are silent.

Quick check. In the level-3 text, which words record that $\delta$ was chosen inside the box of $\varepsilon$ from a line that mentions $\varepsilon$ only?

Solution. The parenthesis “(depending on $\varepsilon$ only)”.

8.3.5. It suffices to show, as a column

Section 8.2 read “it suffices to show $\varphi$ ” as a step that replaces the goal by $\varphi$ and shows on the spot that $\varphi$ is enough. A proof that makes several such steps in a row is easiest to plan, and to check, as a column. The goal goes at the top. Each row is a claim from which the row above follows, with the reason beside it. At the bottom is a claim that needs no reduction: a hypothesis, a fact or a cited result. Read upwards, the column is the proof.

Example (Two columns)

(a) Prove that $x^2 - 6x + 10 > 0$ for every real $x$ . (b) Let $a_n \mathrel{:=} (2n + 1)/(n + 1)$ for $n \in \mathbb{N}$ . Prove that $a_n \to 2$ . Plan each proof as a column of reductions, then write it.

Solution. (a)

It suffices to show	because
$x^2 - 6x + 10 > 0$	(the goal)
$(x - 3)^2 + 1 > 0$	$x^2 - 6x + 10 = (x - 3)^2 + 1$
$(x - 3)^2 \ge 0$	a number at least $0$ , plus $1$ , is positive
—	every square is at least $0$

(b) Let $\varepsilon > 0$ . For $n \in \mathbb{N}$ with $n \ge N$ , where $N$ is still to be chosen:

It suffices to show	because
$\left\| a_n - 2 \right\| < \varepsilon$	(the goal, for $n \ge N$ )
$1/(n + 1) < \varepsilon$	$a_n - 2 = -1/(n + 1)$ , so $\left\| a_n - 2 \right\| = 1/(n + 1)$
$n + 1 > 1/\varepsilon$	for positive numbers, taking reciprocals reverses $<$
$N > 1/\varepsilon$	$n \ge N$ gives $n + 1 > N$
—	choose an integer $N > 1/\varepsilon$ (the school fact of Example (The reciprocals tend to zero)); since $1/\varepsilon > 0$ , $N > 0$ , so $N \in \mathbb{N}$ ; it depends on $\varepsilon$

Each reason is an implication that points up: the row implies the row above it. Read from the bottom, (a) is the proof “Since $(x - 3)^2 \ge 0$ , $x^2 - 6x + 10 = (x - 3)^2 + 1 \ge 1 > 0$ .” Read the same way, (b) is “Let $\varepsilon > 0$ , and choose $N \in \mathbb{N}$ with $N > 1/\varepsilon$ . For $n \ge N$ , $\left| a_n - 2 \right| = 1/(n + 1) < 1/N < \varepsilon$ .” In (b) the constant is found at the bottom of the column, last, and written in the proof’s first sentence, as step 5 of Section 8.5 will require.

Quick check. In column (b), which row introduces a constant, and which reason needs $\varepsilon > 0$ ?

Solution. The bottom row introduces $N$ , chosen from the school fact at $1/\varepsilon$ , so it depends on $\varepsilon$ . The reciprocal row needs $\varepsilon > 0$ : $1/\varepsilon$ must exist and be positive for “ $n + 1 > 1/\varepsilon$ gives $1/(n + 1) < \varepsilon$ ”. The bottom row uses it too: $1/\varepsilon$ must be defined, and an integer above $1/\varepsilon$ lies in $\mathbb{N}$ because $1/\varepsilon > 0$ .

8.3.6. Expand to check

The levels are not only a way to write. They are a way to check. When a sentence of a level-3 proof leaves you uneasy, rewrite that stretch, and only that stretch, at level 1. Either every line of the expansion is legal, and the doubt is settled, or one line breaks a rule, and you have found the error and its exact address.

Start with a sentence whose fault is close to the surface:

Some element of $A$ is positive; let $x$ be one. Since $x$ was arbitrary, every element of $A$ is positive.

Expand it. “Some element of $A$ is positive” is the line $\exists x\, (x \in A \wedge x > 0)$ ; “let $x$ be one” opens an $\mathrm{\exists E}$ box with a fresh name $x_0$ ; “since $x$ was arbitrary” needs a $\mathrm{\forall I}$ . At level 1, with that line marked:

\exists x \, (x \in A \wedge x > 0)

x_0

x_0 \in A \wedge x_0 > 0

x_0 \in A

asm, for

\mathrm{{{\to}}I}

x_0 > 0

\mathrm{{\wedge}E}

x_0 \in A \to x_0 > 0

\mathrm{{{\to}}I}

3–4

\forall x \, (x \in A \to x > 0)

\forall

I? 2–5

Line 6 is what “since $x$ was arbitrary” needs, and no rule gives it. It cannot cite the box 2–5, which is still open (and is the $\mathrm{\exists E}$ box of $x_0$ ); and a new $\mathrm{\forall I}$ box flagged $x_0$ , opened inside it, breaks the side condition of $\mathrm{\forall I}$ (Definition 5.4.1), because $x_0$ appears in the open assumption on line 2. That assumption says that $x_0$ is positive, so $x_0$ is one particular element, not an arbitrary one. Section 8.6 catalogues the error as (N3). For $A = \{-1, 1\}$ the premise is true and the conclusion false.

Here is a harder one, which sounds like the level-3 proof of Example (Uniformly continuous implies continuous, at four levels) run backwards.

Let $\varepsilon > 0$ . For each $x \in A$ , continuity at $x$ gives some $\delta > 0$ such that $\left| f(x) - f(y) \right| < \varepsilon$ for every $y \in A$ with $\left| x - y \right| < \delta$ . Hence, choosing $\delta$ as above for every $x$ , we have $\left| f(x) - f(y) \right| < \varepsilon$ whenever $x, y \in A$ and $\left| x - y \right| < \delta$ , so $f$ is uniformly continuous on $A$ .

Expand it. “Let $\varepsilon > 0$ ” opens a box for $\varepsilon_0$ . “For each $x \in A$ ” opens a box for $x_0$ . “Continuity at $x$ gives some $\delta$ ” is $\mathrm{\forall E}$ twice and the opening of an $\mathrm{\exists E}$ box for $\delta_0$ . At level 1, with the line the sentence needs as line 7, its rule marked with a question mark:

\forall x \in A \; \forall \varepsilon > 0 \; \exists \delta > 0 \; \forall y \in A \; (\left| x - y \right| < \delta \to \left| f(x) - f(y) \right| < \varepsilon)

\varepsilon_0

\varepsilon_0 > 0

x_0

x_0 \in A

\exists \delta > 0 \; \forall y \in A \; (\left| x_0 - y \right| < \delta \to \left| f(x_0) - f(y) \right| < \varepsilon_0)

\forall

E twice 1, 3, 2

\delta_0

\delta_0 > 0

\forall y \in A \; (\left| x_0 - y \right| < \delta_0 \to \left| f(x_0) - f(y) \right| < \varepsilon_0)

\forall x \in A \; \forall y \in A \; (\left| x - y \right| < \delta_0 \to \left| f(x) - f(y) \right| < \varepsilon_0)

\forall

I? 3–6

Line 7 is what the phrase “choosing $\delta$ as above for every $x$ ” needs: one $\delta_0$ that works for all $x$ and $y$ , so that $\mathrm{\exists I}$ can then produce UC’s $\exists \delta$ inside the box of $\varepsilon_0$ . But line 7 would be a $\mathrm{\forall I}$ over $x_0$ , and no such step is legal here. The box of $x_0$ opened at line 3 is still open, so $\mathrm{\forall I}$ cannot cite it; and a new box with the flag $x_0$ , opened inside the box of $\delta_0$ , breaks the side condition of $\mathrm{\forall I}$ (Definition 5.4.1), because $x_0$ appears in the open assumptions on lines 3 and 6. The phrase “for every $x$ ” has generalized over a name on which the chosen $\delta_0$ depends. This is the first blocked line of Example (The search from C to UC), met there in the search; here it was found by expanding one English sentence. Section 8.6 catalogues the error, and Example (The square function on the real line) shows that no repair is possible: for $x^2$ on $\mathbb{R}$ the conclusion is false.

The expansion took six lines, and it was enough to expand the one doubtful stretch. That is the general pattern: you never need to rewrite a whole proof at level 0 to check it. Find the sentence you do not trust, find the boxes open at that sentence, and write the few lines it stands for.

Remark (Looking ahead). From Analysis on the Real Line, Chapter 1 on, proofs are written at level 3, and a rule tag appears only where the rule is itself the point; Sets, Relations, and Cardinality, Chapters 1–3 may still tag some proofs at level 2.

8.3.7. Exercises

A. Check your understanding

Exercise (A1)

Parts (a)–(c) are about Example (Uniformly continuous implies continuous, at four levels), parts (d) and (e) about Example (The irrationality of the square root of two at four levels).

(a) Which lines of the level-1 skeleton does the level-3 sentence “Let $x \in A$ and $\varepsilon > 0$ ” stand for? Which open a box, which close one, and which are written at level 3?
(b) Where is the dependence of $\delta$ recorded at levels 1 and 3?
(c) State the idea of the proof in two sentences.
(d) At which line of levels 1, 2 and 3 is the “not both even” clause of (L) used to reach the contradiction?
(e) True or false, with a reason: at level 3, the sentence “hence $r^2 \ne 2$ ” may be left out of the proof of Theorem 2.2.1, since the reader has just been told that a contradiction was reached.

Solution. (a) Lines 2, 3, 9 and 10. Lines 2 and 3 open the flagged boxes of $x_0$ and $\varepsilon_0$ , with their bounds $x_0 \in A$ and $\varepsilon_0 > 0$ ; lines 9 and 10 close them by $\mathrm{\forall I}$ . The openings are written (“let”); the closings are silent at level 3 (Definition 8.3.2).

(b) At level 1: the box of $\delta_0$ sits inside the boxes of $x_0$ and $\varepsilon_0$ , and line 4, the line it comes from, mentions $\varepsilon_0$ only. At level 3: the parenthesis “(depending on $\varepsilon$ only)”.

(c) Uniform continuity at $\varepsilon$ provides one $\delta$ that serves all pairs of points of $A$ at once, and it provides it before any point is named. Continuity at a point $x$ asks only for the pairs whose first point is $x$ , so the same $\delta$ works.

(d) Level 1: it is the second conjunct of $L(r_0, p_0, q_0)$ on line 8, used at line 11. Level 2: “while they were chosen not both even: a contradiction”. Level 3: “Thus $p$ and $q$ are both even, a contradiction”, where the clash refers back to “not both even” in the sentence that chose $p$ and $q$ .

(e) False. “Hence $r^2 \ne 2$ ” is the conclusion of $\mathrm{\neg I}$ , which Definition 8.3.2 puts among the steps that are never silent. A contradiction alone does not say which assumption it refutes; in this proof the boxes of $p$ , $q$ and of $r^2 = 2$ are all open when it is reached, and the sentence says which box closes and what it gives.

Exercise (A2: Drill)

Each part takes a line or two. (a) names a level; (b)–(f) decide whether a step may be silent at level 3; (g) and (h) judge a text; (i) and (j) decide whether a line may be justified TAUT; (k) and (l) work with an “it suffices to show” column.

(a) “Let $\varepsilon > 0$ [ $\mathrm{\forall I}$ ]. Take $\delta \mathrel{:=} \varepsilon/2$ [ $\mathrm{\exists I}$ ]. …” At which level is this text written?
(b) At level 3, may “since $x$ was arbitrary” be left out?
(c) May “choose $k$ with $n = 2k$ ” be left out?
(d) May “by the triangle inequality” be left out?
(e) May “in particular $x > 0$ ”, after “since $0 < x < 1$ ”, be left out?
(f) May the split “ $x \ge 0$ or $x < 0$ , and every real $x$ is one or the other” be left out?
(g) A skeleton has the line “ $\left| f(x) - f(y) \right| < \varepsilon$ , arith”. Is the proof finished?
(h) A text says “Let $r$ be rational. Then $p$ is even.” Name two never-silent steps that are missing.
(i) From Section 6.3 on, may the level-1 line $x_0 > 0$ , citing the line $x_0 > 0 \wedge y_0 > 0$ , be justified TAUT?
(j) May the line $\forall y\, \forall x\, R(x, y)$ , citing $\forall x\, \forall y\, R(x, y)$ , be justified TAUT?
(k) A column for “ $2^{n+1} > n + 1$ , given $2^n > n$ and $n \ge 1$ ” has the first row “it suffices to show $2^n + 2^n > n + 1$ ”. What is that row’s reason, and what row could come next?
(l) In an “it suffices to show” column, which row is proved outright, with no further reduction?

Solution.

(a) Level 2: sentences, each tagged with the rule it carries.
(b) Yes: it is the closing of $\mathrm{\forall I}$ .
(c) No: it is an $\mathrm{\exists E}$ with a fresh name.
(d) No: it is a citation.
(e) Yes: it is $\mathrm{\wedge E}$ .
(f) No: it is the split of $\mathrm{\vee E}$ , with the reason it exhausts.
(g) No: a skeleton is a plan, and every arith line must be expanded (the warning “A skeleton is not a finished proof”).
(h) The choice of $p$ ( $\mathrm{\exists E}$ with a fresh name, citing (L)): $p$ appears from nowhere. Also missing: the assumption $r^2 = 2$ , the opening of $\mathrm{\neg I}$ , and the citation of Theorem 2.1.3 that licenses “ $p$ is even”.
(i) Yes. On the skeleton (Proposition 6.3.1) it is $P \wedge Q \models P$ , true in every row: it is $\mathrm{\wedge E}$ .
(j) No. On the skeleton the two lines are different letters, and $P \models Q$ fails in a row ( $P$ true, $Q$ false). The step needs $\mathrm{\forall E}$ twice and $\mathrm{\forall I}$ twice.
(k) $2^{n+1} = 2 \cdot 2^n = 2^n + 2^n$ ( $\mathrm{{=}E}$ ). Next: “it suffices to show $2^n \ge 1$ ”, because then $2^n + 2^n > n + 2^n \ge n + 1$ by the hypothesis $2^n > n$ .
(l) The bottom row. It is a hypothesis, a fact or a cited result; every other row is reduced to the one below it.

B. Practice

Exercise (B1: Some-all gives all-some, on the natural numbers)

Read Proposition 5.6.2 over the domain $\mathbb{N}$ , with $R(x, y)$ as “ $x \le y$ ”: from $\exists x\, \forall y\, (x \le y)$ , conclude $\forall y\, \exists x\, (x \le y)$ . The premise is true, with the witness $x = 0$ . Write the proof at levels 1, 2 and 3. Your proof must use the premise, although this instance of the conclusion also has a one-line proof, with $x = y$ .

Solution. Level 1. The proof has no arithmetic, so the skeleton is the level-0 derivation of Proposition 5.6.2 with $R(x, y)$ read as $x \le y$ :

\exists x \, \forall y \, (x \le y)

y_0

x_0

\forall y \, (x_0 \le y)

asm, for

\mathrm{{\exists}E}

x_0 \le y_0

\mathrm{{\forall}E}

\exists x \, (x \le y_0)

\mathrm{{\exists}I}

\exists x \, (x \le y_0)

\mathrm{{\exists}E}

1, 2–4

\forall y \, \exists x \, (x \le y)

\mathrm{{\forall}I}

2–5

Level 2.

Let $y \in \mathbb{N}$ [ $\mathrm{\forall I}$ ]. By hypothesis, some natural number is at most every natural number; choose such a number $x_0$ , which depends on nothing, since the hypothesis mentions no $y$ [ $\mathrm{\exists E}$ , $x_0$ fresh]. In particular $x_0 \le y$ [ $\mathrm{\forall E}$ at $y$ ], so some natural number is at most $y$ [ $\mathrm{\exists I}$ with witness $x_0$ ; then $\mathrm{\exists E}$ closes, since this does not mention $x_0$ ]. Since $y$ was arbitrary, every natural number has a natural number at most it [ $\mathrm{\forall I}$ ].

Level 3.

Let $y \in \mathbb{N}$ . By hypothesis, choose $x_0 \in \mathbb{N}$ with $x_0 \le z$ for every $z \in \mathbb{N}$ ; the hypothesis does not mention $y$ , so $x_0$ does not depend on $y$ . In particular $x_0 \le y$ , so $x_0$ is a natural number at most $y$ .

The level-3 text renames the bound variable of the hypothesis to $z$ , so that $y$ can name the fixed number. The witness $x_0$ was chosen inside the box of $y_0$ , but it comes from line 1, which mentions no $y$ ; so it does not depend on $y$ . The one-line proof, “ $y \le y$ , so take $x = y$ ”, is $\mathrm{\exists I}$ with the witness $y$ , which does depend on $y$ . Both prove the conclusion; only the first is an instance of Proposition 5.6.2, and only the first shows that a single $x$ serves every $y$ .

Exercise (B2: Back from prose to a skeleton, with blanks)

Here is a level-3 proof.

Claim. If $n$ is an odd integer, then $8 \mid n^2 - 1$ .

Let $n$ be odd, say $n = 2k + 1$ with $k$ an integer. Then $n^2 - 1 = 4k(k + 1)$ , so it suffices to show that $k(k + 1)$ is even. If $k = 2j$ for an integer $j$ , then $k(k + 1) = 2 \cdot j(2j + 1)$ ; if $k = 2j + 1$ , then $k(k + 1) = 2 \cdot (2j + 1)(j + 1)$ . Either way $k(k + 1) = 2i$ for an integer $i$ , and then $n^2 - 1 = 8i$ .

Work over the domain $\mathbb{Z}$ , with “ $n$ is odd” as $\exists k\, (n = 2k + 1)$ and $8 \mid m$ as $\exists t\, (m = 8t)$ . Here is its level-1 skeleton with nine blanks, labeled (i)–(ix). Name the move, then complete it, and say where the proof uses the fact (E1) of Section 2.1, that every integer is even or odd.

Solution. The move is skeleton first: every box closes by the rule its opening asks for: a “choose” by $\mathrm{\exists E}$ on a line that does not mention the chosen name, the split by $\mathrm{\vee E}$ , “suppose $n$ is odd” by $\mathrm{{\to}I}$ , “let $n$ ” by $\mathrm{\forall I}$ .

Completion: (i) $\exists j\, (k_0 = 2 \cdot j) \vee \exists j\, (k_0 = 2 \cdot j + 1)$ , by (E1) at $k_0$ ; (ii) $\mathrm{\exists E}$ 5, 6–8; (iii) $\mathrm{\exists E}$ 10, 11–13; (iv) $\mathrm{\vee E}$ 4, 5–9, 10–14; (v) $k_0 \cdot (k_0 + 1) = 2 \cdot i_0$ , with $i_0$ fresh; (vi) $\mathrm{\exists E}$ 15, 16–18; (vii) $\mathrm{\exists E}$ 1, 2–19; (viii) $\mathrm{{\to}I}$ 1–20; (ix) $\mathrm{\forall I}$ 1–21.

(E1) enters at line 4; in the prose it is “if $k = 2j$ … if $k = 2j + 1$ ”, whose reason for covering every case is not written, so the given proof is slightly short of level 3 there.

Exercise (B3: A column of reductions)

(a) Prove that $\left| x - 1 \right| + \left| x + 1 \right| \ge 2$ for every real $x$ by an “it suffices to show” column, each row with its reason.
(b) Turn the column into a level-3 proof.
(c) Which reasons in your column are $\mathrm{{=}E}$ steps that level 3 may leave silent?
(d) A student’s column has the row “it suffices to show $\left| x - 1 \right| \ge 1$ and $\left| x + 1 \right| \ge 1$ ”. Is that row’s reason correct? Can the student finish?

Solution. (a)

It suffices to show	because
$\left\| x - 1 \right\| + \left\| x + 1 \right\| \ge 2$	(the goal)
$\left\| 1 - x \right\| + \left\| x + 1 \right\| \ge \left\| (1 - x) + (x + 1) \right\|$	$\left\| x - 1 \right\| = \left\| 1 - x \right\|$ , and $(1 - x) + (x + 1) = 2$ , so the right side is $\left\| 2 \right\| = 2$
—	the triangle inequality, Example (The triangle inequality by cases) with $1 - x$ and $x + 1$ in place of its $x$ and $y$

(c) $\left| x - 1 \right| = \left| 1 - x \right|$ and $(1 - x) + (x + 1) = 2$ : both are $\mathrm{{=}E}$ links of a chain, silent at level 3 (Definition 8.3.2). The citation of the triangle inequality is never silent.

(d) The reason is correct: if both hold, the sum is at least $2$ , so the row implies the goal. But the student cannot finish. The new row is false at $x = \tfrac12$ , where $\left| x - 1 \right| = \tfrac12$ , although the goal holds there ( $\tfrac12 + \tfrac32 = 2$ ). A reduction is legal whenever its arrow points up; it is useful only when the new row is true.

Marking scheme. (10 points) - 3: (a) a column whose every row has an upward-pointing reason, ending in a cited result or a fact (the triangle inequality, or a case split on the sign of $x - 1$ and $x + 1$ ). - 3: (b) a forward level-3 text with the citation written. - 2: (c) the two $\mathrm{{=}E}$ links named as silent, the citation as spoken. - 2: (d) the reason judged correct, and the row shown false at a named $x$ : it fails exactly when $0 < \left| x \right| < 2$ , for instance at $x = \tfrac12$ .

A three-case proof ( $x \le -1$ ; $-1 < x < 1$ ; $x \ge 1$ ) written as a column earns (a) and (b) in full. Fatal errors (0 for the step): a row whose reason points down (“the goal implies the row”); a case split that does not exhaust (N8).

C. Going deeper

Exercise (C1: Arbitrarily close numbers, at two levels)

Consider Proposition 6.2.5: for real numbers $a$ and $b$ , if $\left| a - b \right| < \varepsilon$ for every $\varepsilon > 0$ , then $a = b$ .

(a) Write its proof at level 1, as a skeleton in which school facts about $\left| \cdot \right|$ and $<$ are lines justified “arith”.
(b) Write it at level 3.
(c) Which lines of your skeleton are silent at level 3? Which instance of $\mathrm{\forall E}$ must the level-3 text name, and why?

Solution. (a) The statement is an implication, so the outer box is $\mathrm{{\to}I}$ ; the goal $a = b$ is atomic, and the proof in Section 6.2 opens an $\mathrm{RAA}$ box on $a \ne b$ .

\forall \varepsilon > 0 \; (\left| a - b \right| < \varepsilon)

asm, for

\mathrm{{{\to}}I}

\neg(a = b)

asm, for

\mathrm{RAA}

\left| a - b \right| > 0

arith 2

\left| a - b \right| < \left| a - b \right|

\mathrm{{\forall}E}

1, 3

\neg(\left| a - b \right| < \left| a - b \right|)

arith

\bot

\mathrm{{\neg}E}

4, 5

a = b

\mathrm{RAA}

2–6

\forall \varepsilon > 0 \; (\left| a - b \right| < \varepsilon) \to a = b

\mathrm{{{\to}}I}

1–7

Line 4 is the bounded $\mathrm{\forall E}$ at the term $\left| a - b \right|$ , whose bound $\left| a - b \right| > 0$ is line 3. Line 5 is the school fact that no real number is less than itself.

(b)

Suppose $\left| a - b \right| < \varepsilon$ for every $\varepsilon > 0$ , and suppose, for a contradiction, that $a \ne b$ . Then $\left| a - b \right| > 0$ , so the hypothesis applies with $\varepsilon = \left| a - b \right|$ and gives $\left| a - b \right| < \left| a - b \right|$ ; but no real number is less than itself. Hence $a = b$ .

(c) Only line 8, the closing line of $\mathrm{{\to}I}$ , is silent: “hence if … then $a = b$ ” is not written. Line 5 is not silent: it is one member of the clashing pair of the $\mathrm{\neg E}$ on line 6, and level 3 names it (“no real number is less than itself”). The instance of line 4 must be named, $\varepsilon = \left| a - b \right|$ , because it is not the obvious term: no name in sight is the obvious candidate for $\varepsilon$ , and the whole proof turns on choosing this one. Saying only “by the hypothesis” would leave the reader to find the instance, and that instance is the idea of the proof. The $\mathrm{RAA}$ opening, “suppose, for a contradiction, that $a \ne b$ ”, and its conclusion, “hence $a = b$ ”, are also never silent.

Marking scheme. (10 points) - 2: (a) the $\mathrm{{\to}I}$ box on the hypothesis, and inside it a box opened on $a \ne b$ . - 2: (a) the box closed by $\mathrm{RAA}$ ( $\mathrm{\neg I}$ alone would give only $\neg\neg(a = b)$ ), with $\bot$ as its last line. - 2: (a) the $\mathrm{\forall E}$ at $\left| a - b \right|$ , citing a line $\left| a - b \right| > 0$ . - 2: (b) a level-3 text with the opening of the contradiction, the instance, the clash and “hence $a = b$ ”, and no tags. - 2: (c) the silent line identified, and the instance $\varepsilon = \left| a - b \right|$ said to be named because it is not the obvious term. - Other routes: a $\mathrm{\neg I}$ box on $a \ne b$ followed by $\mathrm{\neg\neg E}$ , or a split on $\left| a - b \right| > 0$ or $\left| a - b \right| = 0$ (arith) whose first case reaches $\bot$ by the same $\mathrm{\forall E}$ and clash and then $a = b$ by $\mathrm{\bot E}$ , while the second gives $a = b$ by arith, earns the 4 points of the first two lines, provided the $\mathrm{\neg\neg E}$ line is written explicitly, or the disjunction of the split is justified (from $\left| a - b \right| \ge 0$ , or by trichotomy). In the split, the case assumption $\left| a - b \right| > 0$ is the line the $\mathrm{\forall E}$ cites for the third line, and for (b) and (c) the opening of the $\mathrm{\neg I}$ box or of the split stands in for the opening of the contradiction. Fatal errors (0 for the step): the box closed by $\neg I$ with the conclusion $a = b$ ; the hypothesis applied at an $\varepsilon$ not known to be positive.

Exercise (C2: Exit check: levels)

Let $(a_n)$ be a sequence of real numbers with $a_n \to L$ , and let $c \ne 0$ be a real number. Here is a level-0 derivation that $c \, a_n \to cL$ , with the definition of a limit as in Example (Five definitions, translated) (a), the hypothesis $c \ne 0$ as premise 2, and two lines of school arithmetic justified “arith”.

\forall \varepsilon > 0 \; \exists N \in \mathbb{N} \; \forall n \in \mathbb{N} \; (n \ge N \to \left| a_n - L \right| < \varepsilon)

\neg(c = 0)

\varepsilon_0

\varepsilon_0 > 0

asm, for

\mathrm{{\forall}I}

\varepsilon_0 / \left| c \right| > 0

arith 2, 3

\exists N \in \mathbb{N} \; \forall n \in \mathbb{N} \; (n \ge N \to \left| a_n - L \right| < \varepsilon_0 / \left| c \right|)

\mathrm{{\forall}E}

1, 4

N_0

N_0 \in \mathbb{N}

asm, for

\mathrm{{\exists}E}

\forall n \in \mathbb{N} \; (n \ge N_0 \to \left| a_n - L \right| < \varepsilon_0 / \left| c \right|)

asm, for

\mathrm{{\exists}E}

n_0

n_0 \in \mathbb{N}

asm, for

\mathrm{{\forall}I}

n_0 \ge N_0 \to \left| a_{n_0} - L \right| < \varepsilon_0 / \left| c \right|

\mathrm{{\forall}E}

7, 8

n_0 \ge N_0

asm, for

\mathrm{{{\to}}I}

\left| a_{n_0} - L \right| < \varepsilon_0 / \left| c \right|

\mathrm{{{\to}}E}

9, 10

\left| c \cdot a_{n_0} - c \cdot L \right| < \varepsilon_0

arith 2, 11

n_0 \ge N_0 \to \left| c \cdot a_{n_0} - c \cdot L \right| < \varepsilon_0

\mathrm{{{\to}}I}

10–12

\forall n \in \mathbb{N} \; (n \ge N_0 \to \left| c \cdot a_n - c \cdot L \right| < \varepsilon_0)

\mathrm{{\forall}I}

8–13

\exists N \in \mathbb{N} \; \forall n \in \mathbb{N} \; (n \ge N \to \left| c \cdot a_n - c \cdot L \right| < \varepsilon_0)

\mathrm{{\exists}I}

6, 14

\exists N \in \mathbb{N} \; \forall n \in \mathbb{N} \; (n \ge N \to \left| c \cdot a_n - c \cdot L \right| < \varepsilon_0)

\mathrm{{\exists}E}

5, 6–15

\forall \varepsilon > 0 \; \exists N \in \mathbb{N} \; \forall n \in \mathbb{N} \; (n \ge N \to \left| c \cdot a_n - c \cdot L \right| < \varepsilon)

\mathrm{{\forall}I}

3–16

Write the proof at level 2 and at level 3. Then say in one sentence how the case $c = 0$ goes.

Solution. Level 2.

Let $\varepsilon > 0$ [ $\mathrm{\forall I}$ ]. Since $c \ne 0$ , $\left| c \right| > 0$ , so $\varepsilon / \left| c \right| > 0$ [arith]. Applying the definition of $a_n \to L$ with $\varepsilon / \left| c \right|$ in place of $\varepsilon$ [ $\mathrm{\forall E}$ ], choose $N \in \mathbb{N}$ , depending on $\varepsilon$ (and on the fixed number $c$ ), such that $\left| a_n - L \right| < \varepsilon / \left| c \right|$ for every $n \ge N$ [ $\mathrm{\exists E}$ , $N$ fresh]. Let $n \in \mathbb{N}$ [ $\mathrm{\forall I}$ ] with $n \ge N$ [assumption for $\mathrm{{\to}I}$ ]. Then $\left| a_n - L \right| < \varepsilon / \left| c \right|$ [ $\mathrm{\forall E}$ , $\mathrm{{\to}E}$ ], so $\left| c\, a_n - cL \right| = \left| c \right| \, \left| a_n - L \right| < \left| c \right| \cdot \frac{\varepsilon}{\left| c \right|} = \varepsilon$ [arith]. So this $N$ works for $\varepsilon$ [ $\mathrm{{\to}I}$ , $\mathrm{\forall I}$ , $\mathrm{\exists I}$ with witness $N$ ; then $\mathrm{\exists E}$ closes]. Since $\varepsilon > 0$ was arbitrary, $c\, a_n \to cL$ [ $\mathrm{\forall I}$ ].

Level 3.

Let $\varepsilon > 0$ . Since $c \ne 0$ , we have $\varepsilon / \left| c \right| > 0$ , so by the definition of $a_n \to L$ , applied with $\varepsilon / \left| c \right|$ , there is $N \in \mathbb{N}$ (depending on $\varepsilon$ and $c$ ) such that $\left| a_n - L \right| < \varepsilon / \left| c \right|$ for every $n \ge N$ . For every $n \ge N$ , $\left| c\, a_n - cL \right| = \left| c \right| \, \left| a_n - L \right| < \left| c \right| \cdot \frac{\varepsilon}{\left| c \right|} = \varepsilon .$ So this $N$ works for $\varepsilon$ , and $c\, a_n \to cL$ .

The case $c = 0$ . Then $c\, a_n = 0 = cL$ for every $n$ , so $\left| c\, a_n - cL \right| = 0 < \varepsilon$ for every $\varepsilon > 0$ and every $n$ , and any $N$ works, for instance $N = 0$ ; the hypothesis $a_n \to L$ is not needed.

At level 3, the silent steps are those Definition 8.3.2 allows: the $\mathrm{\forall E}$ and $\mathrm{{\to}E}$ of lines 9 and 11 at the obvious $n$ (the implication of line 11 is line 9, an instance of the property of the chosen $N_0$ , not of a hypothesis or a result), carried by “for every $n \ge N$ ”, and the closing lines 13, 14, 16 and 17. The $\mathrm{\forall E}$ of line 5 is not silent, because its instance $\varepsilon / \left| c \right|$ is not the obvious one; it is named (“applied with $\varepsilon / \left| c \right|$ ”). The witness of line 15 is named (“this $N$ ”), and its dependence is stated.

Marking scheme. (10 points) - 4: every never-silent step is present at level 3, one point each: $\varepsilon > 0$ fixed first ( $\mathrm{\forall I}$ ); the hypothesis applied at $\varepsilon / \left| c \right|$ , with its positivity justified, and $N$ chosen from it ( $\mathrm{\exists E}$ ); the witness $N$ produced with its dependence on $\varepsilon$ stated ( $\mathrm{\exists I}$ ); $n \ge N$ taken arbitrary ( $\mathrm{\forall I}$ ). - 3: the level-2 tags are correct: $\mathrm{\forall I}$ for $\varepsilon$ and for $n$ , $\mathrm{\forall E}$ at $\varepsilon / \left| c \right|$ , $\mathrm{\exists E}$ for $N$ , $\mathrm{{\to}I}$ for $n \ge N$ , $\mathrm{\exists I}$ for the witness. Deduct one point per wrong or missing tag, down to 0. - 2: no step silent at level 3 beyond those Definition 8.3.2 allows, steps already scored in the first line not counted again; in particular the estimate $\left| c\, a_n - cL \right| = \left| c \right| \, \left| a_n - L \right| < \left| c \right| \cdot \varepsilon / \left| c \right| = \varepsilon$ is written out for an arbitrary $n \ge N$ . - 1: the case $c = 0$ handled, or excluded explicitly with a reason. A level 3 that writes “for every $n \ge N$ ” as the single phrase for $\mathrm{\forall I}$ together with $\mathrm{{\to}I}$ earns the $\mathrm{\forall I}$ point, as in the solution. Fatal errors (0 for the step): $N$ chosen before $\varepsilon$ is fixed; dividing by $\left| c \right|$ in the case $c = 0$ .

Exercise (C3: Back from prose to a skeleton)

Here is a level-3 proof.

Claim. For every integer $n$ , $4 \mid n^2$ or $4 \mid n^2 - 1$ .

Let $n$ be an integer. If $n$ is even, say $n = 2k$ , then $n^2 = 4k^2$ , so $4 \mid n^2$ . If $n$ is odd, say $n = 2k + 1$ , then $n^2 - 1 = 4k^2 + 4k = 4(k^2 + k)$ , so $4 \mid n^2 - 1$ .

Reconstruct its level-1 skeleton. Work over the domain $\mathbb{Z}$ , with “ $n$ is even” as $\exists k\, (n = 2k)$ , “ $n$ is odd” as $\exists k\, (n = 2k + 1)$ and $4 \mid m$ as $\exists t\, (m = 4t)$ . Name the rule that closes each box, and name every step of the skeleton that the prose leaves unsaid.

Hint: The claim is a disjunction for every $n$ . Which disjunct is reached in each case, and by which rule?

Solution. Write $D(n_0)$ for the goal’s instance $\exists t\, (n_0 \cdot n_0 = 4 \cdot t) \vee \exists t\, (n_0 \cdot n_0 - 1 = 4 \cdot t)$ ; in the derivation it is written out.

n_0

\exists k \, (n_0 = 2 \cdot k) \vee \exists k \, (n_0 = 2 \cdot k + 1)

(E1)

\exists k \, (n_0 = 2 \cdot k)

asm, for

\mathrm{{\vee}E}

k_0

n_0 = 2 \cdot k_0

asm, for

\mathrm{{\exists}E}

n_0 \cdot n_0 = 4 \cdot (k_0 \cdot k_0)

arith 3

\exists t \, (n_0 \cdot n_0 = 4 \cdot t)

\mathrm{{\exists}I}

\exists t \, (n_0 \cdot n_0 = 4 \cdot t) \vee \exists t \, (n_0 \cdot n_0 - 1 = 4 \cdot t)

\mathrm{{\vee}I}

\exists t \, (n_0 \cdot n_0 = 4 \cdot t) \vee \exists t \, (n_0 \cdot n_0 - 1 = 4 \cdot t)

\mathrm{{\exists}E}

2, 3–6

\exists k \, (n_0 = 2 \cdot k + 1)

asm, for

\mathrm{{\vee}E}

k_1

n_0 = 2 \cdot k_1 + 1

asm, for

\mathrm{{\exists}E}

n_0 \cdot n_0 - 1 = 4 \cdot (k_1 \cdot k_1 + k_1)

arith 9

\exists t \, (n_0 \cdot n_0 - 1 = 4 \cdot t)

\mathrm{{\exists}I}

\exists t \, (n_0 \cdot n_0 = 4 \cdot t) \vee \exists t \, (n_0 \cdot n_0 - 1 = 4 \cdot t)

\mathrm{{\vee}I}

\exists t \, (n_0 \cdot n_0 = 4 \cdot t) \vee \exists t \, (n_0 \cdot n_0 - 1 = 4 \cdot t)

\mathrm{{\exists}E}

8, 9–12

\exists t \, (n_0 \cdot n_0 = 4 \cdot t) \vee \exists t \, (n_0 \cdot n_0 - 1 = 4 \cdot t)

\mathrm{{\vee}E}

1, 2–7, 8–13

\forall n \, (\exists t \, (n \cdot n = 4 \cdot t) \vee \exists t \, (n \cdot n - 1 = 4 \cdot t))

\mathrm{{\forall}I}

1–14

Line 1 is (E1) at $n_0$ , cited as in B2’s line 4. The boxes close by $\mathrm{\exists E}$ (lines 7 and 13: $D(n_0)$ does not mention $k_0$ or $k_1$ ), $\mathrm{\vee E}$ (line 14) and $\mathrm{\forall I}$ (line 15). The second case box could reuse the name $k_0$ , since the two boxes are siblings; $k_1$ keeps the lines apart. The arithmetic: $(2k_0)^2 = 4k_0^2$ (line 4) and $(2k_1 + 1)^2 - 1 = 4k_1^2 + 4k_1 = 4(k_1^2 + k_1)$ (line 10).

The prose leaves unsaid the disjunction (E1) and its reason for covering every case (as in B2, the proof is slightly short of level 3 there), the two $\mathrm{\vee I}$ steps (silent: each case’s last words, “so $4 \mid n^2$ ” or “so $4 \mid n^2 - 1$ ”, show which disjunct was reached), the $\mathrm{\exists E}$ closings, the $\mathrm{\vee E}$ closing and the $\mathrm{\forall I}$ closing (silent closings). It writes every opening (“let”, “if”, “say”), both witnesses ( $k^2$ and $k^2 + k$ ) and both computations.