6.1  Translating Mathematics: Nested and Bounded Quantifiers

The calculus is now complete: Sections 5.3–5.7 gave a rule for using and a rule for proving each quantifier, and the two rules for equality. Before any of those rules can act on a definition from analysis, the definition has to be written as a formula, and written correctly. The definitions of analysis have three or four quantifiers stacked in a fixed order, most of them carrying a bound such as ε>0 or n≥N, and every bound costs extra lines in a derivation. This section does three things. It translates the standard definitions into formulas, by a procedure that works from the outside in. It turns each quantifier rule into a bounded rule that handles the bound in the same step. And it collects the traps that make a translation wrong, each with a reading that shows the wrong formula wrong.

Remark (Looking back). Section 3.3 turned an argument in words into a derivation, with one key for a whole paragraph. This section does the same for definitions with quantifiers. What is new is the order of the quantifiers and the bounds they carry, which the propositional key never had.

6.1.1. Four pieces in one sentence

“The sequence (an) converges to L” is written an→L, and a first course defines it in one breath: for every ε>0 there is N∈N such that |an−L|<ε for all n≥N. The sentence has three quantifiers, each with a bound (ε>0, N∈N, n∈N), and a fourth condition, n≥N, hidden in “for all n≥N”, which will turn out to sit under an implication. Each piece has a job, and a slip in any piece changes the meaning:

  • drop the bound ε>0, and the challenger may choose ε=−1; then |an−L|<−1 is impossible, and no sequence converges;
  • swap “for every ε” and “there is N”, and one N must serve every ε; then only sequences that are eventually equal to L converge;
  • read “for all n≥N” as “for all n”, and the first terms must already be close to L; then 1,12,13,… converges to nothing.

So translation deserves a procedure, and the rules deserve a form that handles bounds without fuss. We take them in that order.

6.1.2. Translation from the outside in

Find the outermost claim, name its quantifier and its bound, then translate what it claims about each object, in the same way.

The procedure, in three steps:

  1. Fix the domain. State what the variables range over. The logic of this book has a single domain for all the variables of a formula. Mathematics often mixes kinds of objects in one sentence: in “for every ε>0 there is an N∈N such that for every n≥N, …”, the letter ε is a real number, while N and n are natural numbers. The convention is: the domain is the larger kind (here R), and the smaller kind enters as a bound (∃N∈N, ∀n∈N). So the sentence begins ∀ε>0∃N∈N∀n∈N(n≥N→…), and n ranges over real numbers that happen to be required, by the bound, to be natural numbers. A sequence (an) becomes a function symbol a, with a(n), written an, the n-th term. Its values at real numbers that are not natural numbers are never used, because a is only ever applied to variables bounded by n∈N. Section 5.1 stated this convention in one sentence (“Mixing kinds of number”); here it is in full, and every translation in this chapter follows it.
  2. Find the outermost claim. Ask what the sentence says first, before any detail: “every ε>0 has a property”, “there is an M with a property”, “no prime is largest”. That gives the outermost quantifier (or connective) and its bound.
  3. Recurse. Translate the property, which is a sentence about the object just quantified, by the same two steps. Stop at atomic formulas: equations, inequalities, membership, and predicate symbols such as Prime(m).

A bound is attached to its own quantifier with the connective of Definition 5.1.1: → under ∀, ∧ under ∃. The bounded notation ∀ε>0, ∃N∈N does this automatically, which is why we use it.

A mixed stage. Halfway through, a translation is part words and part symbols, and writing that stage down catches most slips. Take “for every positive ε, some element of A lies within ε of s”. Each line below translates one more quantifier and leaves the rest in words, in square brackets, until no words are left: ∀ε>0[some element of A lies within ε of s]∀ε>0∃x∈A[x lies within ε of s]∀ε>0∃x∈A(|x−s|<ε) Read the last line back, symbol by symbol, into words: if the words are the sentence you began with, the translation is done.

Example (Five definitions, translated)

Translate each sentence into a formula, stating the domain.

  • (a) an→L: for every ε>0 there is N∈N such that |an−L|<ε for every n≥N.
  • (b) The set A of real numbers is bounded above.
  • (c) The function f:R→R is continuous at a: for every ε>0 there is δ>0 such that |f(x)−f(a)|<ε for every real x with |x−a|<δ.
  • (d) There is no largest prime.
  • (e) Every integer greater than 1 has a prime divisor.

Solution. (a) Domain R. The outermost claim is about every ε>0: ∀ε>0. What it says about ε is that some natural number N works: ∃N∈N. What it says about N is that every natural number n from N on is good: ∀n∈N, with the further condition n≥N under an implication. So ∀ε>0∃N∈N∀n∈N(n≥N→|an−L|<ε). The phrase “for every n≥N” carries two bounds on n, membership in N and n≥N; the first is a bounded quantifier, the second the hypothesis of the implication. The free variable is L (and the statement is also about the function symbol a, which is not a variable).

(b) Domain R; A names a set of reals, and x∈A is a one-place predicate of x (Section 5.1). “Bounded above” means that some real number is at least every element of A. Outermost claim: there is an M. Its property: every element of A is at most M: ∃M∀x∈A(x≤M). The bound x∈A belongs to the ∀; there is no bound on M, which may be any real number.

(c) Domain R, with f a one-place function symbol and a a variable, free in the formula: ∀ε>0∃δ>0∀x(|x−a|<δ→|f(x)−f(a)|<ε). The last quantifier has no bound of the form “x∈ something”, because f is defined on all of R; its restriction |x−a|<δ goes under the implication, like n≥N in (a). For f defined on a set A, the last quantifier would be ∀x∈A.

(d) Domain N, with Prime(m) the predicate “m is prime”. Section 5.1 read the sentence as ¬∃m(Prime(m)∧∀n(Prime(n)→n≤m)). A mathematician more often states it positively, “for every prime there is a larger prime”: ∀m(Prime(m)→∃n(Prime(n)∧m<n)). The two forms say the same thing over N: the laws of Section 6.2 push the ¬ inside and give ∀m(Prime(m)→∃n(Prime(n)∧¬(n≤m))), and the order fact that ¬(n≤m) is the same as m<n finishes the job. (That last step is a fact about the order of N, not a law of logic.)

(e) Domain Z. Outermost claim: every integer greater than 1 has a property, ∀n>1. The property: some m is prime and divides n. “Divides” is itself a quantifier: m∣n means n=m⋅k for some integer k. So ∀n>1∃m(Prime(m)∧∃k(n=m⋅k)). Unfolded, the first bound is ∀n(n>1→…). The innermost quantifier came from a defined word, “divides”, which is typical: a definition in words often hides quantifiers, and a translation unfolds them.

Two remarks on the example. First, the order of the quantifiers in (a) and (c) is the order in which the objects are chosen: ε first, by a challenger; then N or δ, by the defender, knowing ε; then n or x, by the challenger again, knowing both. That is the game reading of Example (Swapping two quantifiers). Second, in (c) the letter a is free, so the formula is a statement about a; “f is continuous at every point” would add ∀a in front.

Quick check. Translate “A has a maximum” (an element of A that is at least every element of A) over R. Which quantifier carries the bound x∈A, and does the other quantifier carry a bound too?

Solution. ∃m∈A∀x∈A(x≤m). The bound x∈A belongs to the ∀: “every element of A”. The ∃ carries a bound too, m∈A, because a maximum must itself lie in A; dropping it gives ∃m∀x∈A(x≤m), which is “A is bounded above”, a weaker statement. For A=(0,1) the weaker statement is true (m=1) and the stronger one is false.

Warning. Three mistranslations to avoid. (1) An ∃ with → under it, such as ∃x(x∈A→x>5): it is true as soon as something lies outside A (Section 5.1). (2) A bound on the wrong quantifier: “f is bounded on A” is ∃M∀x∈A(|f(x)|≤M); the form ∃M∈A∀x(|f(x)|≤M) asks for a bound that lies in A and works on all of R, and it fails for f(x)=x on A=[0,1], which is bounded on A by 1. (3) “For all large n” read as “for all n”: “an>0 for all large n” is ∃N∈N∀n∈N(n≥N→an>0), not ∀n∈N(an>0). The sequence an=n−3 satisfies the first (take N=4) and not the second (a0=−3).

6.1.3. Five traps

The warning above caught three slips. Here are five more, each with the reading that shows the wrong formula saying something else.

Example (Five traps, each with a separating reading)

The domain is R unless the row says N. A and B are sets of reals, and x∈A is a one-place predicate (Section 5.1).

Sentence Wrong Right A reading that separates them
(a) Some natural number lies strictly between 13 and 23. ∃n(13<n∧n<23) ∃n∈N(13<n∧n<23) The domain is R, by step 1. The sentence is false, since 0<13 and 23<1; the wrong formula is true, with n=12. Under one domain, a letter for a natural number ranges over the reals unless its bound n∈N says otherwise.
(b) Every element of A and of B is positive. ∀x((x∈A∧x∈B)→x>0) ∀x((x∈A∨x∈B)→x>0) A={1}, B={−1}: the sentence is false (−1∈B). The wrong formula speaks only of common elements, and there are none, so it is true. The “and” of the sentence is an “or” in the restriction.
(c) Only even numbers are multiples of 4. (Over N.) ∀n(Even(n)→4∣n) ∀n(4∣n→Even(n)) The right formula is true; the wrong one is false at n=2. “Only E are M” puts E after the arrow, as “only if” did in Section 1.1.
(d) If a natural number is divisible by 6, then it is even. (Over N.) ∃n(6∣n)→Even(n) ∀n(6∣n→Even(n)) The right formula is true. In the wrong one the last n is free, and read at n=1 it says “if some number is divisible by 6, then 1 is even”: the hypothesis is true (6∣6) and the conclusion false. “A … it” hides a “for every”.
(e) If any element of A is negative, then 0 is not a lower bound of A. ∀x∈A(x<0)→¬∀x∈A(0≤x) ∃x∈A(x<0)→¬∀x∈A(0≤x) A=∅: the right formula is true, since its hypothesis is false. In the wrong one the hypothesis “every element of ∅ is negative” is true and the conclusion “not every element of ∅ is at least 0” is false (Section 5.1, the empty set). This is Section 5.1’s warning on “any”, now with the reading that separates the two formulas: the empty set.

A reading like these is a counter-reading for the step from one formula to the other; it shows that the two say different things, which is all a translation needs to know.

Infinitely many, and eventually. “an>0 for infinitely many n” says that however far out you start, some later term is positive: ∀N∈N∃n∈N(n≥N∧an>0). “Eventually an>0”, that is, an>0 for all large n (warning (3) above), says ∃N∈N∀n∈N(n≥N→an>0). The quantifiers are swapped, and the bound n≥N moves from ∧ to →, as the two connectives of Definition 5.1.1 require. For an=(−1)n the first is true (every even n≥N will do) and the second is false (every odd n≥N fails).

Quick check. Translate “an=0 for only finitely many n”.

Solution. From some index on, no term is 0: ∃N∈N∀n∈N(n≥N→an≠0). Finitely many exceptions all lie below some N.

Translation error or derivation error? When a derivation ends in a statement you believe false, there are two places to look. A derivation error is an illegal line, and checking the derivation line by line finds it. A translation error is a formula that does not say what its sentence says, and no line check finds it, because every line may be correct. Suppose a reader translates “some element of A exceeds 5” as ∃x(x∈A→x>5), the slip of warning (1) above, and takes A={1,2}. From the true line ¬(7∈A), two steps derive that formula: 7∈A→7>5 by Proposition 2.1.2, then ∃I at 7. Both steps are legal. The conclusion is a true formula about A, and the sentence it was meant to translate is false, since neither 1 nor 2 exceeds 5. The fault is in the translation, not in the derivation. So check a surprising conclusion in two ways: run the line check, and read the formulas back into words.

6.1.4. Rules for bounded quantifiers

Every analysis formula has bounds, and each bound doubles the work of a rule. To use ∀ε>0φ at the term 1, ∀E gives 1>0→φ[1/ε], and a second step, →E with a line 1>0, gives φ[1/ε]. To prove ∃N∈Nψ with the witness 7, ∧I builds 7∈N∧ψ[7/N] and ∃I finishes. Every step is legal and every step is predictable, and a derivation about limits drowns in them. So we fold each pair into one step.

A bounded quantifier gets a rule of its own: the bound travels with the quantifier.

Proposition 6.1.1 (Rules for Bounded Quantifiers)

Let A be a fixed set, so that ∈A is a one-place predicate symbol (Section 5.2), x a variable and φ a formula. The following four rules, the bounded rules, may be used in derivations, with the rule names of the unbounded rules and the same side conditions: in ∀x∈AE and ∃x∈AI, the term t is free for x in φ; in ∀x∈AI, the name x0 appears in no premise, in no assumption of a box still open at line k, and not in ∀x∈Aφ; in ∃x∈AE, it appears in no premise, in no assumption of a box still open at line k, and not in χ or in ∃x∈Aφ. The last line of each box is a line of that box itself.

i∀x∈Aφ
jt∈A
kφ[t/x]∀E i, j
it∈A
jφ[t/x]
k∃x∈Aφ∃I i, j
ix0x0∈Aasm, for ∀I
⋮
jφ[x0/x]
k∀x∈Aφ∀I i–j
h∃x∈Aφ
ix0x0∈Aasm, for ∃E
jφ[x0/x]asm, for ∃E
⋮
lχ
kχ∃E h, i–l

Every use of a bounded rule can be replaced by a block of steps of the unbounded rules (Sections 5.3–5.6) and of Chapter 1, with the same premises, the same assumptions open, and the same last line. Hence any derivation that uses the bounded rules converts into one that does not. The same holds with x∈A and t∈A replaced by x>a and t>a, or by the bounds ≥a, <a, ≤a, for a term a in which x does not occur.

In words: to use “every x in A has φ”, produce an element t of A and conclude φ for t. To prove “some x in A has φ”, exhibit an element t of A with φ. To prove “every x in A has φ”, let x0 be an arbitrary element of A (the box opens with the assumption x0∈A) and prove φ for it. To use “some x in A has φ”, take such an element x0, with both facts about it as assumptions, and derive something that does not mention it. These are exactly the sentences a mathematician writes: “let ε>0”, “since δ>0, the hypothesis applies to δ”, “take N=7∈N”, “choose δ>0 such that …”.

The bounded ∀I box is the only flagged box with an assumption that closes by ∀I. Its assumption x0∈A mentions the flag, and that is allowed: the side condition asks about assumptions of boxes still open at line k, and the box’s own assumption has closed there.

In a finished derivation, the assumption x0∈A of a bounded ∀I box is printed “asm, for ∀I”, since the box closes by ∀I.

Second readingWhy a proposition, not a definition

Why is this a proposition and not simply a definition? Because the calculus is fixed: its rules are those of Chapters 1–2 and Sections 5.3–5.7, and a new rule is admissible only if it adds no derivable sequents. Definition 2.3.1 gave one way to show that: a proved sequent, written with statement letters, may be used as one line. It does not cover these rules. The bounded ∀E and ∃I are one line each, but they are schemas in a formula, a variable and a term, not in statement letters; the bounded ∀I and ∃E close boxes, which no proved sequent can. So the proposition proves admissibility the direct way: each bounded step is shown to be an abbreviation of a block of unbounded steps. In this sense the bounded rules are derived rules, in a looser sense that extends Chapter 2’s: a line citing one abbreviates a block of primitive steps, not a proved sequent.

Idea. A bounded quantifier is an abbreviation (Definition 5.1.1): ∀x∈Aφ is the formula ∀x(x∈A→φ), and ∃x∈Aφ is ∃x(x∈A∧φ). So each bounded rule should be an unbounded rule on the unfolded formula, plus the connective rule that handles → or ∧. Write the block, then check two things: the block is a correct piece of derivation wherever the bounded step was, and its side conditions hold exactly when the bounded ones do.

Warning (Not allowed: the bounded rules). Each step below is wrong; the tag names the condition of Proposition 6.1.1 that it breaks.

  • From ∀ε>0φ alone, write φ[1/ε]: the bounded ∀E cites two lines, and the line 1>0 is missing.
  • From |a7−L|<1 alone, write ∃N∈N(|aN−L|<1): the bounded ∃I needs the line 7∈N too.
  • Close a bounded ∀I box on ε0 while the assumption δ0<ε0 of an enclosing box is still open: the flag appears in an assumption of a box still open.
  • Close a bounded ∃E box on N0 with the last line N0+1∈N: the conclusion χ mentions the witness.

The proof writes out, for each bounded rule, the block of unbounded steps it abbreviates, and checks that the side conditions match; it is in the fold below.

Second readingThe proof: each bounded rule as a block of unbounded steps

Proof. We give the replacement block for each rule and check it. In each block, the lines of the bounded version keep their labels, and new lines get new letters.

Bounded ∀E. Line i is ∀x(x∈A→φ). Replace line k by two lines:

i∀x(x∈A→φ)
jt∈A
mt∈A→φ[t/x]∀E i
kφ[t/x]→E m, j

Line m is ∀E at t: the formula (x∈A→φ)[t/x] is t∈A→φ[t/x] by Definition 5.2.5, since A is not a variable. Its side condition asks that t be free for x in x∈A→φ (Definition 5.2.6), which holds exactly when t is free for x in φ, since x∈A has no quantifier. Lines i and j are available at m and k because they were available at k.

Bounded ∃I. Replace line k by:

it∈A
jφ[t/x]
mt∈A∧φ[t/x]∧I i, j
k∃x(x∈A∧φ)∃I m

Line m is the instance at t of x∈A∧φ, and t is free for x there exactly when it is free for x in φ.

Bounded ∀I. Replace the box and line k by a flagged box with no assumption, which contains a →I box holding the old lines:

ix0x0∈Aasm, for →I
⋮
jφ[x0/x]
mx0∈A→φ[x0/x]→I i–j
k∀x(x∈A→φ)∀I i–m

The lines between i and j are unchanged. Each of them lies inside both new boxes, so every line it cited is still available (Definition 1.4.2, with the flagged boxes of Section 5.4): a line outside the old box is outside both new ones, and a line inside the old box is inside the new →I box. The side conditions inside the old box are unaffected too: a line inside it has the same open assumptions as before, x0∈A (now the assumption of the →I box) together with the outer ones, because the flagged box adds none; so every flagged box that closes inside the old box still meets its side condition. Line m is →I, and it is the last line of the flagged box, as ∀I requires; it is the instance at x0 of x∈A→φ. Now the side condition of ∀I at line k: the premises are the same as before; the boxes still open at line k are the same as those open at line k in the bounded version, because the →I box on x0∈A has closed before line k; and the conclusion is the same formula. So the unbounded side condition holds exactly when the bounded one does.

Bounded ∃E. Line h is ∃x(x∈A∧φ). Replace the box’s two assumptions by one assumption and two lines of ∧E:

h∃x(x∈A∧φ)
gx0x0∈A∧φ[x0/x]asm, for ∃E
ix0∈A∧E g
jφ[x0/x]∧E g
⋮
lχ
kχ∃E h, g–l

Lines i and j now hold the same formulas as the old assumptions, inside the same box, so every line that cited them may still cite them. At a line inside the box, the open assumptions are now g together with the outer ones, where before they were x0∈A and φ[x0/x] together with the outer ones. A name appears in g exactly when it appears in x0∈A or in φ[x0/x], so every flagged box that closes inside the box still meets its side condition. The box assumes the instance at x0 of x∈A∧φ, as ∃E requires. Its side condition at line k names χ, the formula ∃x(x∈A∧φ), the premises and the assumptions open at line k: the same four things as the bounded side condition, with the same result.

For the bounds x>a and the others, the same four blocks work with x>a and t>a in place of x∈A and t∈A. One point needs the hypothesis that x does not occur in a: then (x>a)[t/x] is t>a, and the bound contains no bound variable, so free-for conditions are unaffected by it.

Replacing the bounded steps one at a time, each by its block, removes them all; the premises and the last line do not change. This proves the proposition.

Each block is one line longer than the bounded step it replaces: two lines for one in ∀E and ∃I; the extra →I line in ∀I; three lines (an assumption and two ∧E) for two assumptions in ∃E. So each bounded step saves exactly one line, and a derivation with many bounds saves many. More than the count, the bounded rules keep the derivation at the level at which a mathematician thinks: “let ε>0” is one step, not two.

Quick check. Unfolded, ∃N∈Nψ is ∃N(N∈N∧ψ). A student uses the bounded ∃E on it and writes the box with the single assumption N0∈N∧ψ[N0/N]. Is that wrong?

Solution. No, it is the unbounded ∃E, which is always available, since the bounded formula is the unfolded one. It costs two ∧E lines inside the box to separate N0∈N from ψ[N0/N]. The bounded rule opens the box with the two assumptions already separated. Both are correct; the bounded one is shorter by one line.

6.1.5. A limit derivation with bounds

Here is the first derivation in the book about a limit. The claim is the school fact “if an→L, then 2an→2L”, with the definition of Example (Five definitions, translated) (a).

Claim. Over R, ∀ε>0∃N∈N∀n∈N(n≥N→|an−L|<ε) derives the same formula with 2⋅an and 2⋅L in place of an and L, using two lines of arithmetic, justified “arith”: ε0>0 gives ε0/2>0, and |an0−L|<ε0/2 gives |2⋅an0−2⋅L|<ε0 (because |2u−2v|=2|u−v|).

Idea. Run the search. The goal starts with ∀ε>0: open a bounded ∀I box, “let ε0>0”. The new goal starts with ∃N∈N: postpone it (the step of Section 5.5), since no witness is in sight. Turn to the premise: it starts with ∀ε>0, and the step of Section 5.3 says to instantiate it at the term the goal needs. Which term? The goal will need |2an−2L|<ε0, which follows from |an−L|<ε0/2: so instantiate at ε0/2, after an “arith” line ε0/2>0 for the bound. That gives an ∃N∈N line: open its ∃E box at once, with a witness N0 (the step of Section 5.6), and let the box’s last line be the current goal. Now the postponed goal has its witness: N0 itself. The remaining goal ∀n∈N(…) opens a bounded ∀I box for n0, and a →I box on n0≥N0 finishes with one ∀E, one →E, and the second “arith” line. This is the pattern of Proposition 5.6.2: fix ε0, obtain N0, choose N0 as the witness.

Two abbreviations show the shape. Write G(N,ε) for ∀n∈N(n≥N→|an−L|<ε), “from N on, every term is within ε of L”, and G2(N,ε) for the same formula with 2⋅an and 2⋅L. The premise is ∀ε>0∃N∈NG(N,ε), and the goal is the same with G2. With the lines that look inside G left as a gap, the derivation is:

1∀ε>0∃N∈NG(N,ε)
2ε0ε0>0asm, for ∀I
3ε0/2>0arith 2
4∃N∈NG(N,ε0/2)∀E 1, 3
5N0N0∈Nasm, for ∃E
6G(N0,ε0/2)asm, for ∃E
⋮
13G2(N0,ε0)
14∃N∈NG2(N,ε0)∃I 5, 13
15∃N∈NG2(N,ε0)∃E 4, 5–14
16∀ε>0∃N∈NG2(N,ε)∀I 2–15

Lines 7–12 are the only lines that look inside G and G2: they unfold G(N0,ε0/2) at a fresh n0 and prove the instance that line 13 folds back into G2(N0,ε0). The derivation in full follows the check below; its lines 1–6 and 13–16 are the lines above, written out.

Quick check. In the outline, line 4 instantiates the premise at ε0/2. Why that term, and not ε0?

Solution. The goal needs |2an−2L|<ε0, which is 2|an−L|<ε0, so it is enough to have |an−L|<ε0/2. The term is read off the goal (Section 5.3’s step), not off the premise. At ε0 the premise would give only |an−L|<ε0, hence |2an−2L|<2ε0, which does not reach the goal.

1∀ε>0∃N∈N∀n∈N(n≥N→|an−L|<ε)
2ε0ε0>0asm, for ∀I
3ε0/2>0arith 2
4∃N∈N∀n∈N(n≥N→|an−L|<ε0/2)∀E 1, 3
5N0N0∈Nasm, for ∃E
6∀n∈N(n≥N0→|an−L|<ε0/2)asm, for ∃E
7n0n0∈Nasm, for ∀I
8n0≥N0→|an0−L|<ε0/2∀E 6, 7
9n0≥N0asm, for →I
10|an0−L|<ε0/2→E 8, 9
11|2⋅an0−2⋅L|<ε0arith 10
12n0≥N0→|2⋅an0−2⋅L|<ε0→I 9–11
13∀n∈N(n≥N0→|2⋅an−2⋅L|<ε0)∀I 7–12
14∃N∈N∀n∈N(n≥N→|2⋅an−2⋅L|<ε0)∃I 5, 13
15∃N∈N∀n∈N(n≥N→|2⋅an−2⋅L|<ε0)∃E 4, 5–14
16∀ε>0∃N∈N∀n∈N(n≥N→|2⋅an−2⋅L|<ε)∀I 2–15

Check the side conditions at the three lines that close flagged boxes, and the witness line.

  • Line 13 (∀n∈NI, flag n0): n0 is not in the premise, not in line 13, and not in the assumptions still open at line 13, which are lines 2, 5, and 6.
  • Line 14 (∃N∈NI): the witness N0, with its bound on line 5 and the instance on line 13.
  • Line 15 (∃N∈NE, flag N0): N0 is not in line 15, the conclusion (the witness has been forgotten by line 14), not in line 4, not in the premise, and not in the open assumption on line 2.
  • Line 16 (∀ε>0I, flag ε0): ε0 is not in the premise and not in line 16, and no assumption is open at line 16.

Line 4 is where N comes to depend on ε: the witness N0 is obtained from the premise at ε0/2, so it depends on ε0, exactly as the order ∀ε∃N allows. Section 6.4 makes this reading of dependence precise.

In prose, line by line:

Let ε>0 [lines 2, 16]. Then ε/2>0 [3], so, since an→L, there is N∈N with |an−L|<ε/2 for every n≥N [4]; choose such an N [5, 6, 15]. Let n∈N with n≥N [7, 9]. Then |an−L|<ε/2 [8, 10], so |2an−2L|=2|an−L|<ε [11]. So this N works [12–14].

Written with the unbounded rules, the same derivation has 22 lines, since each of its six bounded steps (lines 4, 8, 13, 14, 15, and 16) costs one line more. The claim “1n→0” (for n≥1) is not derived here: its proof needs the Archimedean property, a fact about N inside R, not a law of logic.

Remark (Looking ahead). Induction (“a set of natural numbers that contains 0 and contains n+1 whenever it contains n contains every natural number”) and the least-upper-bound property of the real numbers say “for every set of numbers”, and the variables of this chapter range over numbers only. Chapter 7’s optional last section says what that costs.

6.1.6. Exercises

A. Check your understanding

Exercise (A1)
  • (a) Translate into formulas, stating the domain: (i) every real number has a cube root; (ii) the function f is bounded on A; (iii) between any two different real numbers there is a rational number; (iv) the sequence (an) is eventually constant; (v) some natural number divides every natural number.
  • (b) Three students translate “some element of A is larger than every element of B”, over R:
    • (i) ∃x∈A∀y∈B(x>y); (ii) ∃x(x∈A→∀y∈B(x>y)); (iii) ∀y∈B∃x∈A(x>y). Which are correct? For each wrong one, give sets A, B for which it has the wrong truth value.
  • (c) Which variables are free in your answer to (a)(iv)?
  • (d) Write the bounded rule ∃x∈AI as a block of two unbounded steps, and name the two rules.

Solution. (a) (i) Over R: ∀x∃y(y⋅y⋅y=x). (ii) Over R: ∃M∀x∈A(|f(x)|≤M). (iii) Over R, with ∈Q a one-place predicate symbol: ∀x∀y(x<y→∃q∈Q(x<q∧q<y)); “different” is carried by x<y, which names the smaller number x (the case y<x is the same statement with the letters exchanged). (iv) Over R, with a a function symbol: ∃N∈N∀n∈N(n≥N→an=aN). (v) Over N: ∃d∀n∃k(n=d⋅k); it is true, with d=1.

(b) Only (i) is correct. (ii) has → under ∃: with A={0} and B={5}, the sentence in words is false, but (ii) is true, because x=7∉A makes the implication vacuously true. (iii) has the quantifiers in the wrong order: it lets the element of A depend on y. With A=B=N, (iii) is true (for each y, take x=y+1), and the sentence in words is false, since no natural number exceeds every natural number.

(c) None of the variables: N and n are bound. The formula is a statement about the function symbol a, which is not a variable.

(d) From t∈A and φ[t/x]: first t∈A∧φ[t/x] by ∧I, then ∃x(x∈A∧φ) by ∃I, which is ∃x∈Aφ unfolded.

Exercise (A2: Drill)

Each part takes a line or two. The domain is R, and A, B are sets of reals. The parts run from translating, through unfolding and judging, to single steps of the bounded rules.

  • (a) Translate “f is bounded above on A”.
  • (b) Translate “every element of A is less than some element of B”.
  • (c) Translate “some element of A is less than every element of B”.
  • (d) Unfold the bounds of (c).
  • (e) Write the mixed stage, then the formula, for “every element of A has a larger element in A”.
  • (f) Translate “an>0 for all large n”.
  • (g) Translate “an≤0 for infinitely many n”.
  • (h) Translate “not every element of A is positive” and “no element of A is positive”, and decide both for A={−1,1}.
  • (i) Translate “if x⋅x<0 for any real x, then 0=1”.
  • (j) Lines 1 ∀ε>0φ and 2 1>0. What does the bounded ∀E 1, 2 give?
  • (k) Lines 1 3∈N and 2 3+3=6. What does the bounded ∃I 1, 2 give, with φ the formula n+n=6?
  • (l) How many lines does a bounded ∃E save over the unbounded rule?

Solution.

  • (a) ∃M∀x∈A(f(x)≤M).

  • (b) ∀x∈A∃y∈B(x<y).

  • (c) ∃x∈A∀y∈B(x<y).

  • (d) ∃x(x∈A∧∀y(y∈B→x<y)).

  • (e) ∀x∈A[some element of A is larger than x], then ∀x∈A∃y∈A(x<y).

  • (f) ∃N∈N∀n∈N(n≥N→an>0).

  • (g) ∀N∈N∃n∈N(n≥N∧an≤0).

  • (h) ¬∀x∈A(x>0), true for {−1,1} (because of −1); ¬∃x∈A(x>0), or ∀x∈A¬(x>0), false (because of 1). One word apart, opposite truth values.

  • (i) ∃x(x⋅x<0)→0=1: “any” after “if” is “some”. It is true, since no real square is negative.

  • (j) φ[1/ε].

  • (k) ∃n∈N(n+n=6).

  • (l) One: two assumptions in place of one assumption and two ∧E lines.

B. Practice

Exercise (B1: Three definitions)

Formalize each statement, stating the domain and the kind of each symbol (variable, constant, function symbol, predicate symbol; membership ∈A in a fixed set A is a one-place predicate symbol, as in Section 5.2).

  • (a) The set A of real numbers is bounded (above and below).
  • (b) The function f:R→R is increasing on A: for all x,y∈A, x<y implies f(x)≤f(y).
  • (c) The sequence (an) is bounded: there is a real M with |an|≤M for all n.

Then, for (c), write the formula with the two quantifiers in the other order, and say why it holds for every sequence.

Solution. No constants occur in any of the three parts.

(a) Domain R; m, M, x variables (all bound); ∈A a one-place and ≤ a two-place predicate symbol. ∃m∃M∀x∈A(m≤x∧x≤M). The two witnesses are chosen before x, so they must work for every element of A.

(b) Domain R; x, y variables (bound); f a one-place function symbol; ∈A a one-place and <, ≤ two-place predicate symbols. ∀x∈A∀y∈A(x<y→f(x)≤f(y)).

(c) Domain R; M, n variables (bound); a a one-place function symbol (the one-domain convention, step 1 of the procedure), and |⋅| a one-place function symbol; ∈N a one-place and ≤ a two-place predicate symbol. ∃M∀n∈N(|an|≤M).

Swapped: ∀n∈N∃M(|an|≤M). It holds for every sequence, because the witness may depend on n: take M=|an|. The sequence an=n, which is not bounded, satisfies it. As in Example (Swapping two quantifiers), the swap turns a statement about one M for all n into a statement about each term separately.

Exercise (B2: A bounded rehearsal)

Using the bounded rules of Proposition 6.1.1, derive ∀x∈A(P(x)→Q(x)),∃x∈AP(x)⊢∃x∈AQ(x). Then say how many lines the derivation would have with the unbounded rules only.

Solution. The goal is an ∃: postpone it. The second premise is an ∃: open its bounded ∃E box at once, with a witness x0 and the two assumptions x0∈A and P(x0), and aim for the goal as the box’s last line. Inside, the first premise is a ∀x∈A, and the term the box offers is x0, with its bound on a line. The witness for the goal is x0 again.

1∀x∈A(P(x)→Q(x))
2∃x∈AP(x)
3x0x0∈Aasm, for ∃E
4P(x0)asm, for ∃E
5P(x0)→Q(x0)∀E 1, 3
6Q(x0)→E 5, 4
7∃x∈AQ(x)∃I 3, 6
8∃x∈AQ(x)∃E 2, 3–7

At line 8, x0 is not in line 8, not in line 2, and not in either premise; no other box is open. The derivation uses three bounded steps (lines 5, 7 and 8), each of which costs one more line unbounded, so the unbounded derivation has 8+3=11 lines: the ∃E box assumes x0∈A∧P(x0) and splits it with two ∧E lines; line 5 becomes ∀E then →E; line 7 becomes ∧I then ∃I.

The bound is the whole point of the exercise: the witness x0 must carry its membership in A from the premise to the conclusion, and the bounded rules make that one assumption and one citation.

Exercise (B3: One key, twenty sentences)

The domain is N={0,1,2,…}. Use only Prime(x) (“x is prime”), Even(x), x<y, x∣y (“x divides y”, that is, y=x⋅k for some k), = and the constants 1, 2, 9, with variables x, y, z. Translate sentences 1–18 into formulas. Then translate 19 and 20 into English and decide whether each is true.

  1. 2 is an even prime.
  2. Some prime divides 9.
  3. Every prime greater than 2 is odd.
  4. No prime is less than 2.
  5. Every even number is divisible by 2.
  6. Only odd numbers divide 9.
  7. 1 divides every number.
  8. Some number divides every number.
  9. Every number is divisible by some number.
  10. There is no largest prime.
  11. There are infinitely many primes.
  12. Every number greater than 1 has a prime divisor.
  13. The only divisors of a prime are 1 and the prime itself.
  14. If a number divides 2, it is 1 or 2.
  15. Not every odd number is prime.
  16. Between any two numbers, one less than the other, there is a third.
  17. Some prime divides every even number.
  18. Every divisor of 1 is 1.
  19. ∀x∀y((x∣y∧y∣x)→x=y).
  20. ∀x(Even(x)→∃y(Prime(y)∧y∣x∧¬(y=2))).

Solution.

  1. Even(2)∧Prime(2).
  2. ∃x(Prime(x)∧x∣9).
  3. ∀x((Prime(x)∧2<x)→¬Even(x)).
  4. ¬∃x(Prime(x)∧x<2), or ∀x(Prime(x)→¬(x<2)).
  5. ∀x(Even(x)→2∣x).
  6. ∀x(x∣9→¬Even(x)).
  7. ∀x(1∣x).
  8. ∃x∀y(x∣y).
  9. ∀y∃x(x∣y).
  10. ∀x(Prime(x)→∃y(Prime(y)∧x<y)).
  11. ∀x∃y(x<y∧Prime(y)).
  12. ∀x(1<x→∃y(Prime(y)∧y∣x)).
  13. ∀x(Prime(x)→∀y(y∣x→(y=1∨y=x))).
  14. ∀x(x∣2→(x=1∨x=2)).
  15. ¬∀x(¬Even(x)→Prime(x)).
  16. ∀x∀y(x<y→∃z(x<z∧z<y)).
  17. ∃x(Prime(x)∧∀y(Even(y)→x∣y)).
  18. ∀x(x∣1→x=1).
  19. “Two numbers that divide each other are equal.” True in N: if y=xk and x=yl, then x=xkl, so either x=0, and then y=0 too, or kl=1, which in N means k=l=1.
  20. “Every even number has a prime divisor other than 2.” False: at x=2, and at every power of 2 (4,8,16,32,…), the only prime divisor is 2.

Sentence 10 restricts x to primes and 11 does not; both are true, and in N each follows from the other. Sentence 16 is false (take x=0, y=1), and its translation is still correct: a correct translation of a false sentence is a false formula.

Exercise (B4: Unfold, then fold back)

Over R, for fixed sets A, B, C of reals, write A⊆B for “every element of A is an element of B”, A∪B for the set of reals in A or in B, and A∩B for the set of those in both. Use only the predicates ∈A, ∈B, ∈C.

  • (a) Unfold A⊆B∩C.
  • (b) Unfold A∪B⊆C.
  • (c) Unfold “A∩B has no element”.
  • (d) Fold back ∀x(x∈A→x∈B)∧∀x(x∈B→x∈C).
  • (e) Fold back ∀x((x∈A∧x∈B)→x∈C).
  • (f) A reader unfolds A∪B⊆C as the formula in (e). Give sets that separate the two, and say why the reader’s formula is wrong.

Solution. (a) ∀x(x∈A→(x∈B∧x∈C)).

(b) ∀x((x∈A∨x∈B)→x∈C).

(c) ¬∃x(x∈A∧x∈B).

(d) A⊆B and B⊆C.

(e) A∩B⊆C.

(f) A={1}, B={2}, C=∅. Then A∪B⊆C is false, since 1∈A∪B and 1∉C. The formula of (e) is true, because A∩B has no element, so its hypothesis x∈A∧x∈B is false for every x. The reader’s mistake is trap (b) of the section: “in A or in B” is the restriction of (b), and it must be written with ∨; the “and” of “every element of A and of B” is an “or” in the restriction.

Marking scheme. (10 points) - 2: (a)–(c) together, with every bound attached by → under ∀ (and by ∧ under the ∃ of (c)). - 2: (d) and (e). - 3: (f): the two sets, with one sentence on each truth value. - 3: the reason in words that the restriction of (b) is an “or”. Fatal error (0 for (f)): a pair of sets on which the two formulas agree.

C. Going deeper

Exercise (C1: Where the ∀x stands)

Let f:R→R and A⊆R. Translate, over R:

  • (a) f is uniformly continuous on A: for every ε>0 there is δ>0 such that for all x,y∈A, |x−y|<δ implies |f(x)−f(y)|<ε;
  • (b) f is continuous at every point of A: for every x∈A and every ε>0 there is δ>0 such that for every y∈A, |x−y|<δ implies |f(x)−f(y)|<ε.

Then describe, in one sentence, the only difference between the two formulas, and say what it means for the choice of δ.

Solution. (a) ∀ε>0∃δ>0∀x∈A∀y∈A(|x−y|<δ→|f(x)−f(y)|<ε).

(b) ∀x∈A∀ε>0∃δ>0∀y∈A(|x−y|<δ→|f(x)−f(y)|<ε).

The only difference is the position of ∀x∈A: in (a) it stands after ∃δ>0, in (b) before it. In (b) the defender chooses δ knowing x, so δ may depend on x and on ε; in (a) δ is chosen before any x is given, so one δ must serve every x∈A at once, and it depends on ε only. Section 6.4 derives (b) from (a) and shows that x2 on R satisfies (b) but not (a); Section 7.2 turns this example into a counter-model, so (b) does not derive (a).

Exercise (C2: Six orders, four statements)

Fix a formula μ (the “matrix”) in the variables x, y, z, and consider the six sentences obtained by putting the prefixes ∀x, ∃y, ∀z in front of μ in the six possible orders: ∀x∃y∀zμ, ∀z∃y∀xμ, and so on. Call two of these orders essentially the same if the two sentences are provably equivalent (⊣⊢) for every matrix μ, and essentially different if some matrix over Z gives them different truth values (read informally, as in Section 5.1).

  • (a) Show that the six orders fall into four groups, with any two orders in one group essentially the same.
  • (b) Using the matrices y>x and y>z over Z, show that any two orders from different groups are essentially different. So the six orders say four different things.

Solution (Hint 1). Two ∀’s side by side can be exchanged: that was one of the derivations of Example (Flagged boxes at work). What is left to decide is where ∃y stands.

Solution (Hint 2). List the six orders by the position of ∃y: first, middle or last. When it is first or last, the two ∀’s are side by side.

Solution. (a) Sort the orders by the position of ∃y.

  • ∃y first: ∃y∀x∀zμ and ∃y∀z∀xμ.
  • ∃y last: ∀x∀z∃yμ and ∀z∀x∃yμ.
  • ∃y in the middle: ∀x∃y∀zμ, and ∀z∃y∀xμ.

Two adjacent ∀’s may be exchanged: ∀x∀zψ⊣⊢∀z∀xψ for every formula ψ, by the derivation of Example (Flagged boxes at work) that exchanges two universal quantifiers (it uses nothing about its matrix but that it is a formula). This gives the “last” pair at once. For the “first” pair the ∀’s sit under ∃y: open the ∃E box on ∃y∀x∀zμ with a witness y0, exchange the two ∀’s inside it, and close with ∃I at y0; the other direction is the same. So there are at most four groups: {∃y∀x∀z, ∃y∀z∀x}, {∀x∀z∃y, ∀z∀x∃y}, {∀x∃y∀z} and {∀z∃y∀x}.

(b) Call the groups F (∃y first), L (last), Mx (∀x∃y∀z) and Mz (∀z∃y∀x). Over Z, evaluate each group with the two matrices, reading informally (Section 5.1):

Group μ=(y>x) μ=(y>z)
F false: no y exceeds every x false: no y exceeds every z
L true: given x, z, take y=x+1 true: take y=z+1
Mx true: given x, take y=x+1 false: no y exceeds every z
Mz false: no y exceeds every x true: given z, take y=z+1

Every two rows differ in at least one column, so every two groups are separated by one of the two matrices: F from L, from Mx and from Mz by the column in which the other group has “true”; L from Mx by y>z and from Mz by y>x; Mx from Mz by either. So the six orders say four different things: within a group the sentences are provably equivalent by (a), and across groups some matrix over Z tells them apart.

Marking scheme. (10 points) - 2: lists the six orders and sorts them by the position of ∃y. - 3: justifies the two collapses, citing the exchange of adjacent ∀’s, and handles the pair under ∃y (by an ∃E box, or equivalently). - 3: gives, for each of the six pairs of groups, a matrix and the two truth values, with witnesses for the true sentences. - 2: concludes that the six orders say four different things, combining (a) and (b). Fatal errors (0 for the step): exchanging ∀ with ∃; a “separation” in which the two sentences have the same truth value.

Exercise (C3: Eventually, therefore infinitely often)
  • (a) With the bounded rules, derive ∃N∈N∀n∈N(n≥N→P(n))⊢∀M∈N∃n∈N(n≥M∧P(n)). Lines of arithmetic may be justified “arith”.
  • (b) For the converse, give a reading of P over N under which the premise is true and the conclusion false.

Solution. (a) The goal is a bounded ∀: open its box first, with M0∈N. The premise is a bounded ∃: open its box early, with N0∈N and its property. The postponed goal ∃n∈N needs a term that is at least M0 and at which the premise applies, so at least N0: the sum N0+M0 is both.

1∃N∈N∀n∈N(n≥N→P(n))
2M0M0∈Nasm, for ∀I
3N0N0∈Nasm, for ∃E
4∀n∈N(n≥N0→P(n))asm, for ∃E
5N0+M0∈Narith 2, 3
6N0+M0≥N0→P(N0+M0)∀E 4, 5
7N0+M0≥N0arith 2
8P(N0+M0)→E 6, 7
9N0+M0≥M0arith 3
10N0+M0≥M0∧P(N0+M0)∧I 9, 8
11∃n∈N(n≥M0∧P(n))∃I 5, 10
12∃n∈N(n≥M0∧P(n))∃E 1, 3–11
13∀M∈N∃n∈N(n≥M∧P(n))∀I 2–12

Lines 7 and 9 use M0≥0 and N0≥0, which hold for natural numbers. The side conditions:

  • At line 12, N0 is not in line 12, not in line 1, not in the premise, and not in the open assumption on line 2.
  • At line 13, M0 is not in the premise and not in line 13, and no assumption is open.
  • At lines 6 and 11, the term N0+M0 is free for n.

The witness N0+M0 is built from the two names in play: fix M0, obtain N0, choose a term made from both.

(b) Let P(n) be “n is even”. The premise of the converse, ∀M∈N∃n∈N(n≥M∧P(n)), is true: beyond any M there is an even number, such as 2M. Its conclusion, ∃N∈N∀n∈N(n≥N→P(n)), is false: beyond any N there is an odd number, 2N+1. This is a counter-reading (Section 7.2).

Marking scheme. (10 points) - 2: opens the flagged box of M0 and the ∃E box on the premise (in either nesting) before choosing the witness. - 3: a witness that depends on both names, with both bounds checked by arith lines. - 2: checks the side conditions at lines 12 and 13. - 3: (b): a reading, with both truth values justified. Fatal errors (0 for the step): a witness chosen before M0 is given; the witness N0 itself, which need not be at least M0.