6.2 Negating and Moving Quantifiers

To prove that a sequence does not converge, or that a function is not uniformly continuous, we must use the negation of a definition, and a negation is only usable once the $\neg$ has been pushed all the way in. “It is not the case that for every $\varepsilon > 0$ there is an $N$ …” gives a proof nothing to hold. “There is an $\varepsilon > 0$ such that for every $N$ there is an $n \ge N$ with …” tells it what to find. Section 5.1 read the step from the first form to the second informally, as the challenger and the defender changing sides. This section derives the laws that make it exact, with the rules of Sections 5.3–5.6. Once they are proved, negating a definition is mechanical: one law per symbol, from the outside in. It then shows the laws at work, in an analysis proof in which a negation and a well-chosen $\varepsilon$ do the work, and ends with the laws that move a quantifier across a connective, and with prenex form, where every quantifier stands at the front.

Remark (Looking back). Section 3.2 proved two statements equivalent by two derivations, one each way. Every law of this section is such a pair. What is new is that a law may now be used on a part of a formula buried under quantifiers, and the subsection on negating a definition says why that is safe.

6.2.1. Not every, and some not

Section 5.1 called the two quantifiers mirror images: a single counterexample refutes a “for every”, and a single witness confirms a “there exists”. The mirror suggests four sequents. “Not every $x$ satisfies $\varphi$ ” should say the same as “some $x$ fails $\varphi$ ”, and “no $x$ satisfies $\varphi$ ” the same as “every $x$ fails $\varphi$ ”. Three of the four directions come straight out of the search method. The fourth does not, and the reason it does not is worth a close look.

To negate a quantifier, flip it and move the $\neg$ inside.

In the derivations of this section, $\neg\varphi[x_0/x]$ means $(\neg\varphi)[x_0/x]$ , which is $\neg(\varphi[x_0/x])$ by Definition 5.2.5; the two readings give the same formula. The fresh name $x_0$ is always a variable different from $x$ that does not appear in $\varphi$ (or in $\psi$ , when there is one); so it does not appear in $\forall x\, \varphi$ or $\exists x\, \varphi$ either. The side conditions of $\mathrm{\forall I}$ and $\mathrm{\exists E}$ need this, and it also makes $x_0$ free for $x$ in $\varphi$ (Section 5.2).

Proposition 6.2.1 (Quantifier Negation)

Let $\varphi$ be a formula and $x$ a variable.

(a) $\neg\forall x\, \varphi \vdash \exists x\, \neg\varphi$ , by a derivation that uses $\mathrm{RAA}$ ;
(b) $\exists x\, \neg\varphi \vdash \neg\forall x\, \varphi$ , by a derivation that does not;
(c) $\neg\exists x\, \varphi \dashv\vdash \forall x\, \neg\varphi$ , both directions by derivations that do not use $\mathrm{RAA}$ .

Try it first (ten minutes): run the search method of Section 3.1, with the quantifier steps of Sections 5.3–5.6, on (a). Which rule should give the last line, and what would that rule need from the premise?

Idea. Start with (a), and with the obstacle. The goal $\exists x\, \neg\varphi$ is an $\exists$ , so the search postpones it until an available line shows an instance $\neg\varphi[t/x]$ . None ever does. The premise $\neg\forall x\, \varphi$ is a negation, and a negation is used only by clashing it with what it negates, $\forall x\, \varphi$ . It says that a counterexample exists and names none, so $\mathrm{\exists I}$ has nothing to act on. We are stuck, and the last step of the method applies: assume $\neg\exists x\, \neg\varphi$ , “no $x$ fails $\varphi$ ”, and hunt for a clash. The clash will be with the premise, so the new goal is $\forall x\, \varphi$ . Open a flagged box for it, with the goal $\varphi[x_0/x]$ . That goal is again stuck (we know nothing about $\varphi$ ), so a second $\mathrm{RAA}$ assumes $\neg\varphi[x_0/x]$ ; and now an instance of $\neg\varphi$ is on a line, so $\mathrm{\exists I}$ produces $\exists x\, \neg\varphi$ , which clashes with the outer assumption.

For (b) and (c) the method runs without getting stuck. A negated goal opens a $\mathrm{\neg I}$ box (Section 2.2); an $\exists$ premise opens an $\mathrm{\exists E}$ box early (Section 5.6); a $\forall$ goal opens a flagged box (Section 5.4). The clash comes in one of two ways. In (b), and in (c) right to left, the instance assumed in the $\mathrm{\exists E}$ box clashes with the matching instance that $\mathrm{\forall E}$ takes from the $\forall$ line. In (c) left to right, $\mathrm{\exists I}$ turns the instance into $\exists x\, \varphi$ , which meets the premise $\neg\exists x\, \varphi$ .

Proof. For (a), the derivation:

\neg \forall x\, \varphi

\neg \exists x\, \neg \varphi

asm, for

\mathrm{RAA}

x_0

\neg \varphi[x_0/x]

asm, for

\mathrm{RAA}

\exists x\, \neg \varphi

\mathrm{{\exists}I}

\bot

\mathrm{{\neg}E}

4, 2

\varphi[x_0/x]

\mathrm{RAA}

3–5

\forall x\, \varphi

\mathrm{{\forall}I}

3–6

\bot

\mathrm{{\neg}E}

7, 1

\exists x\, \neg \varphi

\mathrm{RAA}

2–8

Line 4 is $\mathrm{\exists I}$ at the term $x_0$ , which is free for $x$ in $\neg\varphi$ . At line 7 the side condition of $\mathrm{\forall I}$ holds: $x_0$ does not appear in the premise, in the assumption $\neg\exists x\, \neg\varphi$ still open at line 7, or in $\forall x\, \varphi$ , since it is not $x$ and does not appear in $\varphi$ ; and line 6 is the last line of the flagged box.

For (b):

\exists x\, \neg \varphi

\forall x\, \varphi

asm, for

\mathrm{{\neg}I}

x_0

\neg \varphi[x_0/x]

asm, for

\mathrm{{\exists}E}

\varphi[x_0/x]

\mathrm{{\forall}E}

\bot

\mathrm{{\neg}E}

4, 3

\bot

\mathrm{{\exists}E}

1, 3–5

\neg \forall x\, \varphi

\mathrm{{\neg}I}

2–6

At line 6, $x_0$ does not appear in $\bot$ , in $\exists x\, \neg\varphi$ , in the premise, or in the assumption $\forall x\, \varphi$ still open there.

For (c), left to right and right to left:

\neg \exists x\, \varphi

x_0

\varphi[x_0/x]

asm, for

\mathrm{{\neg}I}

\exists x\, \varphi

\mathrm{{\exists}I}

\bot

\mathrm{{\neg}E}

3, 1

\neg \varphi[x_0/x]

\mathrm{{\neg}I}

2–4

\forall x\, \neg \varphi

\mathrm{{\forall}I}

2–5

\forall x\, \neg \varphi

\exists x\, \varphi

asm, for

\mathrm{{\neg}I}

x_0

\varphi[x_0/x]

asm, for

\mathrm{{\exists}E}

\neg \varphi[x_0/x]

\mathrm{{\forall}E}

\bot

\mathrm{{\neg}E}

3, 4

\bot

\mathrm{{\exists}E}

2, 3–5

\neg \exists x\, \varphi

\mathrm{{\neg}I}

2–6

In the first, line 5 is the instance of $\neg\varphi$ at $x_0$ , as $\mathrm{\forall I}$ requires, and $x_0$ appears neither in the premise nor in $\forall x\, \neg\varphi$ ; no assumption is open at line 6. In the second, the side condition of $\mathrm{\exists E}$ at line 6 is checked as in (b). No line of the derivations of (b) and (c) is justified by $\mathrm{RAA}$ , and the derivation of (a) uses it twice, at lines 6 and 9. This proves the proposition.

So “not every” and “some not” are interderivable, and so are “none” and “every not”. The direction that cost two $\mathrm{RAA}$ boxes is the one that produces an existential statement from a negative one. That is not an accident of our derivation: no derivation of (a) avoids $\mathrm{RAA}$ . This is a claim about all derivations, which no search can establish, and we state it without proof (Chapter 4’s optional Theorem 4.7.4 proves the propositional analogue for $\neg\neg P \vdash P$ ).

Quick check. From the line $\neg\forall x\, P(x)$ , may a derivation write $\neg P(c)$ for a constant $c$ ? If not, what may it write, and what does a derivation do next to use it?

Solution. No. $\neg\forall x\, P(x)$ says that some element fails $P$ , not that the element named $c$ does: over $\mathbb{Z}$ , with $P$ read as “is even” and $c$ as $0$ , $\neg\forall x\, P(x)$ is true and $\neg P(0)$ is false. By (a) the derivation may write $\exists x\, \neg P(x)$ . To use that line it opens an $\mathrm{\exists E}$ box with a fresh witness $x_0$ and the assumption $\neg P(x_0)$ (Section 5.6), and nothing about $c$ follows.

The laws as one line. From now on a derivation may use any law of this section as one line, citing it, in the way Proposition 6.1.1 allows a bounded rule: the line abbreviates the derivation printed here, with $\varphi$ (and $\psi$ ) replaced by the formulas at hand and the fresh name chosen so that it appears nowhere in the larger derivation. Then every side condition inside the pasted block still holds, since the block’s premises become lines of the larger derivation and the name is new to all of them. In a derivation the justification is a short tag: QN (a) for Proposition 6.2.1 (a), NIm for Proposition 6.2.2 below, and VI for Proposition 2.1.2.

6.2.2. The negation of an implication

Every definition with a bounded $\forall$ contains an implication, $\forall x\, (x \in A \to \varphi)$ , so negating it means negating an implication. The answer is the one Section 5.1 found for the wrong translation of a bounded $\exists$ : an implication fails exactly when its hypothesis holds and its conclusion does not. Chapter 3 met this law only as an exercise (Exercise (B1: Three searches) (b)), and a proof in the text may not rest on an exercise, so we prove it here.

Proposition 6.2.2 (Negated Implication)

For all formulas $\varphi$ and $\psi$ , $\neg(\varphi \to \psi) \dashv\vdash \varphi \wedge \neg\psi .$ The direction $\vdash$ is derived with $\mathrm{RAA}$ , and the direction $\dashv$ without it.

Idea. For $\vdash$ the goal is a conjunction, so $\mathrm{\wedge I}$ asks for $\varphi$ and $\neg\psi$ separately. The premise is a negation, usable only to clash with $\varphi \to \psi$ , so in each part we manufacture $\varphi \to \psi$ . For $\neg\psi$ : open a $\mathrm{\neg I}$ box on $\psi$ ; then $\varphi \to \psi$ follows by $\mathrm{{\to}I}$ , whose box repeats $\psi$ . For $\varphi$ we are stuck, since $\varphi$ has no known main connective; so $\mathrm{RAA}$ assumes $\neg\varphi$ , and $\neg\varphi$ gives $\varphi \to \psi$ by Proposition 2.1.2. For $\dashv$ , the goal is a negation: assume $\varphi \to \psi$ and clash $\psi$ with $\neg\psi$ .

Proof. The two derivations:

\neg (\varphi \to \psi)

\neg \varphi

asm, for

\mathrm{RAA}

\varphi \to \psi

VI 2

\bot

\mathrm{{\neg}E}

3, 1

\varphi

\mathrm{RAA}

2–4

\psi

asm, for

\mathrm{{\neg}I}

\varphi

asm, for

\mathrm{{{\to}}I}

\psi

\mathrm{R}

\varphi \to \psi

\mathrm{{{\to}}I}

7–8

\bot

\mathrm{{\neg}E}

9, 1

\neg \psi

\mathrm{{\neg}I}

6–10

\varphi \wedge \neg \psi

\mathrm{{\wedge}I}

5, 11

\varphi \wedge \neg \psi

\varphi \to \psi

asm, for

\mathrm{{\neg}I}

\varphi

\mathrm{{\wedge}E}

\psi

\mathrm{{{\to}}E}

2, 3

\neg \psi

\mathrm{{\wedge}E}

\bot

\mathrm{{\neg}E}

4, 5

\neg (\varphi \to \psi)

\mathrm{{\neg}I}

2–6

Line 3 of the first derivation uses Proposition 2.1.2 as a derived rule (Definition 2.3.1), and line 8 repeats line 6 into the box, since $\mathrm{{\to}I}$ needs $\psi$ as a line of its own box. The only $\mathrm{RAA}$ is at line 5.

The derivations use only the rules of Chapters 1 and 2, so the law holds for statements as well as formulas, and it may be used as a derived rule in the sense of Definition 2.3.1. Over the real numbers: “if $x > 2$ then $x^2 > 4$ ” fails for a given $x$ exactly when $x > 2$ and $x^2 \le 4$ .

6.2.3. Bounded quantifiers keep their bounds

Analysis negates bounded quantifiers: $\neg\forall \varepsilon > 0$ , $\neg\exists N \in \mathbb{N}$ . The two laws so far combine into laws for them, and the combination has one surprise in it, which is no surprise once the bound is unfolded: the bound stays as it is.

Negating a bounded quantifier flips the quantifier and keeps the bound.

Proposition 6.2.3 (Negating Bounded Quantifiers)

Let $A$ be a fixed set, so that $\in A$ is a one-place predicate symbol, let $x$ be a variable and $\varphi$ a formula. Then

(a) $\neg\forall x \in A \; \varphi \dashv\vdash \exists x \in A \; \neg\varphi$ , where $\vdash$ is derived with $\mathrm{RAA}$ and $\dashv$ without;
(b) $\neg\exists x \in A \; \varphi \dashv\vdash \forall x \in A \; \neg\varphi$ , both directions without $\mathrm{RAA}$ .

The same holds with $x \in A$ replaced by $x > a$ , or by $x \ge a$ , $x < a$ , $x \le a$ , for a term $a$ in which $x$ does not occur.

So $\neg\forall \varepsilon > 0\; \varphi$ becomes $\exists \varepsilon > 0\; \neg\varphi$ , and never $\exists \varepsilon \le 0\; \neg\varphi$ .

Idea. Unfold the bounds (Definition 5.1.1): (a) is $\neg\forall x\, (x \in A \to \varphi) \dashv\vdash \exists x\, (x \in A \wedge \neg\varphi)$ . Push the $\neg$ through the quantifier by Proposition 6.2.1, and then through the implication by Proposition 6.2.2; the second step must happen under the $\exists$ , so it happens inside an $\mathrm{\exists E}$ box. The negation lands on $\varphi$ , and the bound $x \in A$ comes out of the implication unnegated. For (b), the derivations of Proposition 6.2.1 (c) go through with the bounded rules of Proposition 6.1.1 in place of the unbounded ones.

Proof. For (a), $\vdash$ and $\dashv$ , with the bounds unfolded:

\neg \forall x\, (x \in A \to \varphi)

\exists x\, \neg (x \in A \to \varphi)

QN (a) 1

x_0

\neg (x_0 \in A \to \varphi[x_0/x])

asm, for

\mathrm{{\exists}E}

x_0 \in A \wedge \neg \varphi[x_0/x]

NIm 3

\exists x\, (x \in A \wedge \neg \varphi)

\mathrm{{\exists}I}

\exists x\, (x \in A \wedge \neg \varphi)

\mathrm{{\exists}E}

2, 3–5

\exists x\, (x \in A \wedge \neg \varphi)

x_0

x_0 \in A \wedge \neg \varphi[x_0/x]

asm, for

\mathrm{{\exists}E}

\neg (x_0 \in A \to \varphi[x_0/x])

NIm 2

\exists x\, \neg (x \in A \to \varphi)

\mathrm{{\exists}I}

\exists x\, \neg (x \in A \to \varphi)

\mathrm{{\exists}E}

1, 2–4

\neg \forall x\, (x \in A \to \varphi)

QN (b) 5

Line 3 on the left is the instance at $x_0$ of $\neg(x \in A \to \varphi)$ , since $A$ is not a variable; line 4 is Proposition 6.2.2 with $x_0 \in A$ and $\varphi[x_0/x]$ for $\varphi$ and $\psi$ . At line 6, $x_0$ does not appear in the conclusion, in line 2 or in the premise, and no assumption is open. The right-hand derivation is checked the same way. The only use of $\mathrm{RAA}$ is inside the two cited laws on the left: in QN (a) and in the direction $\vdash$ of NIm.

For (b), with the bounded rules:

\neg \exists x \in A \; \varphi

x_0

x_0 \in A

asm, for

\mathrm{{\forall}I}

\varphi[x_0/x]

asm, for

\mathrm{{\neg}I}

\exists x \in A \; \varphi

\mathrm{{\exists}I}

2, 3

\bot

\mathrm{{\neg}E}

4, 1

\neg \varphi[x_0/x]

\mathrm{{\neg}I}

3–5

\forall x \in A \; \neg \varphi

\mathrm{{\forall}I}

2–6

\forall x \in A \; \neg \varphi

\exists x \in A \; \varphi

asm, for

\mathrm{{\neg}I}

x_0

x_0 \in A

asm, for

\mathrm{{\exists}E}

\varphi[x_0/x]

asm, for

\mathrm{{\exists}E}

\neg \varphi[x_0/x]

\mathrm{{\forall}E}

1, 3

\bot

\mathrm{{\neg}E}

4, 5

\bot

\mathrm{{\exists}E}

2, 3–6

\neg \exists x \in A \; \varphi

\mathrm{{\neg}I}

2–7

At line 7 on the left, the box’s own assumption $x_0 \in A$ has closed, and $x_0$ is in neither the premise nor the conclusion; at line 7 on the right, $x_0$ is not in $\bot$ , in line 2, in the premise, or in the open assumption on line 2. Neither derivation uses $\mathrm{RAA}$ .

For the bounds $x > a$ and the others, the same four derivations work with $x > a$ and $x_0 > a$ in place of $x \in A$ and $x_0 \in A$ , choosing $x_0$ not to appear in $a$ ; since $x$ does not occur in $a$ , $(x > a)[x_0/x]$ is $x_0 > a$ . This proves the proposition.

Warning. Negate the quantifier, not the bound. The negation of “ $a_n \to L$ ” begins $\exists \varepsilon > 0$ , not $\exists \varepsilon \le 0$ . The wrong form, $\exists \varepsilon \le 0\; \forall N \in \mathbb{N}\; \exists n \in \mathbb{N}\; (n \ge N \wedge \left| a_n - L \right| \ge \varepsilon)$ , is true for every sequence: $\varepsilon = 0$ works, since $\left| a_n - L \right| \ge 0$ always. So it would “prove” that the constant sequence $a_n = 0$ does not converge to $0$ .

6.2.4. Negating a definition, mechanically

With the laws in hand, negating a definition is a procedure.

Algorithm. Negating a formula.

Rewrite $\leftrightarrow$ as two implications, by Proposition 2.4.1.
Push $\neg$ inward, one symbol at a time, from the outside, citing a law at each step:
- $\neg\forall x$ becomes $\exists x\, \neg$ , and $\neg\exists x$ becomes $\forall x\, \neg$ (Proposition 6.2.1); a bounded quantifier keeps its bound (Proposition 6.2.3);
- $\neg(\alpha \to \beta)$ becomes $\alpha \wedge \neg\beta$ (Proposition 6.2.2);
- $\neg(\alpha \wedge \beta)$ becomes $\neg\alpha \vee \neg\beta$ , and $\neg(\alpha \vee \beta)$ becomes $\neg\alpha \wedge \neg\beta$ (De Morgan, Proposition 2.5.5);
- $\neg\neg\alpha$ becomes $\alpha$ (Proposition 2.5.1).
Stop at atomic formulas. In an ordered domain, replace $\neg(s < t)$ by $s \ge t$ and $\neg(s \le t)$ by $s > t$ ; these are facts about the order, not laws of logic.

Each step of 1 and 2 replaces a part of the formula by a part provably equivalent to it. Write that chain with $\dashv\vdash$ between the stages, not $\equiv$ . Step 3 is not a law of logic: make its replacements after the chain, citing the order fact.

Why may a step act on a part buried inside the formula? Because a part may be replaced by a part provably equivalent to it, even under quantifiers that bind its variables, as long as the equivalence is derivable for every choice of those variables, that is, its closure is derivable.

Proposition 6.2.4 (Replacement of Provable Equivalents)

Let $\varphi$ and $\psi$ be formulas, and let $z_1, \dots, z_k$ be the variables free in $\varphi$ or in $\psi$ . Suppose that $\vdash \forall z_1 \cdots \forall z_k\, (\varphi \leftrightarrow \psi)$ . If $\chi'$ is obtained from a formula $\chi$ by replacing one occurrence of $\varphi$ in $\chi$ by $\psi$ , then $\vdash \forall w_1 \cdots \forall w_m\, (\chi \leftrightarrow \chi')$ , where $w_1, \dots, w_m$ are the variables free in $\chi$ or in $\chi'$ . In particular, $\chi \dashv\vdash \chi'$ .

In words: swap a part for a provably equivalent part anywhere in a formula, provided the equivalence is derivable for every choice of its free variables, that is, its closure is derivable; every law of this section is.

The proof is an induction on the formula $\chi$ ; its connective steps are short derivations with the rules of Chapters 1 and 2, its quantifier steps use a flagged box or an $\mathrm{\exists E}$ box with a fresh name, and it does not use truth tables or completeness. It is in the fold below, followed by a second fold that checks the hypothesis for the laws of this section.

Second readingThe proof of the replacement rule

Proof. For a formula $\theta$ , write $\overline{\forall}\theta$ for its closure: $\theta$ preceded by one $\forall$ for each variable free in $\theta$ . The order of these $\forall$ ’s does not matter, because the instance of $\forall z_1 \cdots \forall z_k\,\theta$ at fresh flags comes by $\mathrm{\forall E}$ in that order, and $k$ flagged boxes closed by $\mathrm{\forall I}$ in any other order give the $\forall$ ’s in that other order (this is the derivation of Example (Flagged boxes at work) (c), with $k$ variables), so “the closure” means the closure in any one order. The hypothesis is $\vdash \overline{\forall}(\varphi \leftrightarrow \psi)$ , and the claim is $\vdash \overline{\forall}(\chi \leftrightarrow \chi')$ . A derivable formula may stand as a line of any derivation: paste its derivation in, with its flags renamed to names new to the whole derivation, as “The laws as one line” allows.

We use strong induction (Theorem 4.2.2) on the number of connectives and quantifier symbols of $\chi$ : assume the claim for every formula with fewer such symbols, and prove it for $\chi$ .

Case 0: the occurrence is $\chi$ itself. Then $\chi$ is $\varphi$ , $\chi'$ is $\psi$ , and the claim is the hypothesis.

Otherwise the occurrence lies in an immediate part of $\chi$ , which has fewer symbols; an atomic formula has no part other than itself.

Case 1: $\chi = \neg\chi_0$ , with the occurrence in $\chi_0$ , so $\chi' = \neg\chi_0'$ . The induction hypothesis gives $\vdash \overline{\forall}(\chi_0 \leftrightarrow \chi_0')$ . Open one flagged box for each variable of the closure of $\neg\chi_0 \leftrightarrow \neg\chi_0'$ , nested in the closure’s order, with fresh flags. Inside, $\mathrm{\forall E}$ of the induction hypothesis at the flags, each variable at its own flag in the closure’s order, gives the instance $\alpha \leftrightarrow \alpha'$ of $\chi_0 \leftrightarrow \chi_0'$ at the flags; every variable of that closure is free in $\chi$ or $\chi'$ , so it has a flag. The rules of Sections 2.2 and 2.4 give $\neg\alpha \leftrightarrow \neg\alpha'$ : each direction is a $\mathrm{\neg I}$ box (Definition 2.2.1) with $\mathrm{\leftrightarrow E}$ inside, and $\mathrm{\leftrightarrow I}$ (Definition 2.4.1) joins them. The flagged boxes then close by $\mathrm{\forall I}$ , the innermost first. Each side condition holds: the flag is fresh, and no assumption is open at the closing line.

Case 2: $\chi = \chi_1 \circ \chi_2$ , where $\circ$ is $\wedge$ , $\vee$ , $\to$ or $\leftrightarrow$ , and the occurrence is in $\chi_1$ (in $\chi_2$ , exchange the parts). As in case 1, with the propositional step $\alpha \leftrightarrow \alpha' \vdash (\alpha \circ \gamma) \leftrightarrow (\alpha' \circ \gamma)$ , where $\gamma$ is the instance of $\chi_2$ at the flags. For each $\circ$ it is a short derivation with that connective’s rules of Chapters 1 and 2 and $\mathrm{\leftrightarrow E}$ on $\alpha \leftrightarrow \alpha'$ . A variable free in $\chi$ but not in $\chi_1$ is flagged and never instantiated, which is harmless: the instance of the induction hypothesis is taken at the flags of its own variables only.

Case 3: $\chi = \forall x\, \chi_0$ or $\exists x\, \chi_0$ , with the occurrence in $\chi_0$ , so $\chi'$ is $\forall x\, \chi_0'$ or $\exists x\, \chi_0'$ . The induction hypothesis gives $\vdash \overline{\forall}(\chi_0 \leftrightarrow \chi_0')$ , whose closure may include $x$ . Let $\bar w$ be the variables free in $\chi$ or $\chi'$ , so $x$ is not among them, flag them with fresh names $\bar w_0$ , and write $\theta_0$ for $\theta[\bar w_0/\bar w]$ . Substitution passes $\forall x$ and $\exists x$ , because $x$ is not among $\bar w$ ; and all the flags are fresh, so the simultaneous and the step-by-step substitutions agree.

For $\forall$ , left to right: assume $\forall x\, (\chi_0)_0$ and open a flagged box with a fresh $x_1$ . Use $\mathrm{\forall E}$ at $x_1$ . Use $\mathrm{\forall E}$ of the induction hypothesis at $\bar w_0$ and $x_1$ , each variable at its own flag in the closure’s order. Then $\mathrm{\leftrightarrow E}$ gives $(\chi_0')_0[x_1/x]$ , and $\mathrm{\forall I}$ gives $\forall x\, (\chi_0')_0$ . The flag $x_1$ is in no premise, open assumption or conclusion.
Right to left is the same, and $\mathrm{\leftrightarrow I}$ joins the two directions.
For $\exists$ : an $\mathrm{\exists E}$ box with a fresh witness $x_1$ , $\mathrm{\leftrightarrow E}$ inside, closed after $\mathrm{\exists I}$ .

The flagged boxes of $\bar w_0$ then close by $\mathrm{\forall I}$ , as in case 1.

The “in particular”. From $\vdash \overline{\forall}(\chi \leftrightarrow \chi')$ , $\mathrm{\forall E}$ at each $w_i$ itself (a variable is free for itself) gives $\chi \leftrightarrow \chi'$ , and $\mathrm{\leftrightarrow E}$ gives each direction. No truth table and no completeness theorem was used.

Second readingWhy the laws of this section meet the hypothesis

A law of this section is proved for every formula that meets its condition, so it holds for the instances at fresh names $z_{1,0}, \dots, z_{k,0}$ , and $\mathrm{\leftrightarrow I}$ (Definition 2.4.1) joins the two directions into $\alpha \leftrightarrow \beta$ at the fresh names, and $k$ flagged boxes give its closure, as Proposition 6.2.4 asks. Take one variable $x$ at a time, with sides $\alpha$ and $\beta$ of the law, and a fresh $x_0$ : a variable other than $x$ that appears in neither $\alpha$ nor $\beta$ . The derivation of $\alpha[x_0/x] \vdash \beta[x_0/x]$ is available because each law used holds for every formula that meets its condition, in particular for the instances at $x_0$ . The laws this book applies to parts have conditions of two kinds, and both survive, for the same reason; the passage laws at the end of this section have one kind, checked in the fold after them, and the bounded negation laws the other. A law of Proposition 6.2.3 with a bound such as $z > a$ asks that its bound variable $z$ not occur in the term $a$ ; since $z$ appears in $\beta$ , $x_0$ is not $z$ (as for the passage laws, in the fold after them). If $z$ is $x$ , substitution stops at the quantifier on $x$ and the pair is unchanged; otherwise it passes the quantifier on $z$ , and $a[x_0/x]$ contains no variable that $a$ lacks except $x_0$ , so $z$ does not occur in it. So the instance is again an instance of the same law, with its condition met.

Renaming a bound variable is a replacement of this kind: Section 5.4 derived $\forall y\, \varphi \dashv\vdash \forall z\, \varphi[z/y]$ for every formula $\varphi$ in which $z$ does not appear (the fold after Example (Flagged boxes at work)), and Section 5.6 did the same for $\exists$ , so the convention of Section 5.2, that a renaming may be made anywhere inside a formula, is now a provable equivalence. Its closure is derivable, as Proposition 6.2.4 asks: for a variable $x$ free in it and a fresh $x_0$ (as in the fold above), $x$ is neither $y$ nor $z$ , and $x_0$ is not $z$ , because $z$ appears in $\forall z\, \varphi[z/y]$ , so $z$ does not appear in $\varphi[x_0/x]$ , and the instance is the renaming of $\forall y\, \varphi[x_0/x]$ to $\forall z\, \varphi[x_0/x][z/y]$ . Two formulas that differ only by renaming bound variables are joined by a chain of single renamings, each to a letter absent from the formula at that step (for $\forall x\, \forall y\, R(x, y)$ and $\forall y\, \forall x\, R(y, x)$ : $x$ to $u$ , then $y$ to $x$ , then $u$ to $y$ ), each applied to a part by Proposition 6.2.4 and chained by Lemma 2.3.3.

Example (Three negations from analysis)

Negate each statement into positive form: no $\neg$ in front of a quantifier, a connective or an inequality. Work over $\mathbb{R}$ .

(a) $a_n \to L$ : $\forall \varepsilon > 0 \; \exists N \in \mathbb{N} \; \forall n \in \mathbb{N} \; \bigl( n \ge N \to \left| a_n - L \right| < \varepsilon \bigr)$ .
(b) $s$ is the supremum of $A$ , in the two-clause form “ $s$ is an upper bound of $A$ , and for every $\varepsilon > 0$ some element of $A$ exceeds $s - \varepsilon$ ”: $\forall x \in A \; (x \le s) \;\wedge\; \forall \varepsilon > 0 \; \exists x \in A \; (s - \varepsilon < x) .$
(c) $f$ is uniformly continuous on $A$ : $\forall \varepsilon > 0 \; \exists \delta > 0 \; \forall x \in A \; \forall y \in A \; \bigl( \left| x - y \right| < \delta \to \left| f(x) - f(y) \right| < \varepsilon \bigr)$ .

Solution. (a) Three quantifiers, then an implication, then an inequality: $\begin{aligned} &\neg \forall \varepsilon > 0 \; \exists N \in \mathbb{N} \; \forall n \in \mathbb{N} \; \bigl( n \ge N \to \left| a_n - L \right| < \varepsilon \bigr) \\ \dashv\vdash\; &\exists \varepsilon > 0 \; \neg \exists N \in \mathbb{N} \; \forall n \in \mathbb{N} \; \bigl( n \ge N \to \left| a_n - L \right| < \varepsilon \bigr) \\ \dashv\vdash\; &\exists \varepsilon > 0 \; \forall N \in \mathbb{N} \; \neg \forall n \in \mathbb{N} \; \bigl( n \ge N \to \left| a_n - L \right| < \varepsilon \bigr) \\ \dashv\vdash\; &\exists \varepsilon > 0 \; \forall N \in \mathbb{N} \; \exists n \in \mathbb{N} \; \neg \bigl( n \ge N \to \left| a_n - L \right| < \varepsilon \bigr) \\ \dashv\vdash\; &\exists \varepsilon > 0 \; \forall N \in \mathbb{N} \; \exists n \in \mathbb{N} \; \bigl( n \ge N \wedge \neg (\left| a_n - L \right| < \varepsilon) \bigr). \end{aligned}$ The first three steps are Proposition 6.2.3, the fourth is Proposition 6.2.2. Last, the order fact turns $\neg(\left| a_n - L \right| < \varepsilon)$ into $\left| a_n - L \right| \ge \varepsilon$ : $\exists \varepsilon > 0 \; \forall N \in \mathbb{N} \; \exists n \in \mathbb{N} \; \bigl( n \ge N \wedge \left| a_n - L \right| \ge \varepsilon \bigr).$ In words: some $\varepsilon > 0$ is such that, however far out we start, some later term is at least $\varepsilon$ away from $L$ . Every bound stayed, and the order of the quantifiers stayed: $\varepsilon$ , then $N$ , then $n$ .

(b) The outer symbol is $\wedge$ . By De Morgan the negation becomes a disjunction, and each side is negated on its own: $\begin{aligned} &\neg \bigl( \forall x \in A \; (x \le s) \;\wedge\; \forall \varepsilon > 0 \; \exists x \in A \; (s - \varepsilon < x) \bigr) \\ \dashv\vdash\; &\neg \forall x \in A \; (x \le s) \;\vee\; \neg \forall \varepsilon > 0 \; \exists x \in A \; (s - \varepsilon < x) \\ \dashv\vdash\; &\exists x \in A \; \neg (x \le s) \;\vee\; \exists \varepsilon > 0 \; \forall x \in A \; \neg (s - \varepsilon < x). \end{aligned}$ The first step is Proposition 2.5.5, (d) for $\vdash$ and (c) for $\dashv$ ; the second is Proposition 6.2.3, (a) on the left and (a) then (b) on the right. Last, the order facts turn $\neg(x \le s)$ into $s < x$ and $\neg(s - \varepsilon < x)$ into $x \le s - \varepsilon$ : $\exists x \in A \; (s < x) \;\vee\; \exists \varepsilon > 0 \; \forall x \in A \; (x \le s - \varepsilon).$ In words: $s$ fails to be the supremum when some element of $A$ lies above it (it is not an upper bound), or when some $s - \varepsilon$ with $\varepsilon > 0$ is still an upper bound (it is not the least).

(c) Four quantifiers and an implication: $\begin{aligned} &\neg \forall \varepsilon > 0 \; \exists \delta > 0 \; \forall x \in A \; \forall y \in A \; \bigl( \left| x - y \right| < \delta \to \left| f(x) - f(y) \right| < \varepsilon \bigr) \\ \dashv\vdash\; &\exists \varepsilon > 0 \; \forall \delta > 0 \; \exists x \in A \; \exists y \in A \; \neg \bigl( \left| x - y \right| < \delta \to \left| f(x) - f(y) \right| < \varepsilon \bigr) \\ \dashv\vdash\; &\exists \varepsilon > 0 \; \forall \delta > 0 \; \exists x \in A \; \exists y \in A \; \bigl( \left| x - y \right| < \delta \wedge \neg (\left| f(x) - f(y) \right| < \varepsilon) \bigr), \end{aligned}$ where the first step is four uses of Proposition 6.2.3, and the second is Proposition 6.2.2. Last, the order fact turns $\neg(\left| f(x) - f(y) \right| < \varepsilon)$ into $\left| f(x) - f(y) \right| \ge \varepsilon$ : $\exists \varepsilon > 0 \; \forall \delta > 0 \; \exists x \in A \; \exists y \in A \; \bigl( \left| x - y \right| < \delta \wedge \left| f(x) - f(y) \right| \ge \varepsilon \bigr).$ In words: one $\varepsilon > 0$ defeats every $\delta$ : however small $\delta > 0$ is, two points of $A$ closer than $\delta$ have values at least $\varepsilon$ apart. To prove that a function is not uniformly continuous, this is the statement to prove, and it says exactly what to exhibit: first $\varepsilon$ ; then, for an arbitrary $\delta$ , the two points $x$ and $y$ , which may depend on $\delta$ . Section 6.4 does this for $x^2$ on $\mathbb{R}$ .

The same procedure finishes the rewriting promised in Section 6.1 for “there is no largest prime”. By Proposition 6.2.1 (c), $\begin{aligned} &\neg \exists m \; \bigl( \mathrm{Prime}(m) \wedge \forall n \; (\mathrm{Prime}(n) \to n \le m) \bigr) \\ \dashv\vdash\; &\forall m \; \neg \bigl( \mathrm{Prime}(m) \wedge \forall n \; (\mathrm{Prime}(n) \to n \le m) \bigr). \end{aligned}$ A negated conjunction $\neg(\alpha \wedge \beta)$ is interderivable with $\alpha \to \neg\beta$ : De Morgan’s law (Proposition 2.5.5 (d)) and Proposition 2.5.6 (a) give one direction, and (b) of the latter with Proposition 2.5.5 (c) the other. Then Proposition 6.2.1 (a) and (b) turn $\neg\forall n\, (\mathrm{Prime}(n) \to n \le m)$ into $\exists n\, \neg(\mathrm{Prime}(n) \to n \le m)$ , and Proposition 6.2.2, used under $\exists n$ , pushes the last $\neg$ in; both steps act on a part, by Proposition 6.2.4: $\forall m \; \Bigl( \mathrm{Prime}(m) \to \exists n \; \bigl( \mathrm{Prime}(n) \wedge \neg(n \le m) \bigr) \Bigr).$ The quantifier $\forall n\, (\mathrm{Prime}(n) \to \dots)$ works like a bounded one, with the bound $\mathrm{Prime}(n)$ . That bound is not one that Proposition 6.2.3 covers, but the same two steps work for it, and the bound stays unnegated.

Quick check. Negate “every non-empty set of reals that is bounded above has a supremum”, writing $E(A)$ for “ $A$ is non-empty”, $B(A)$ for “ $A$ is bounded above” and $S(A)$ for “ $A$ has a supremum”, with the variable $A$ ranging over sets of reals.

Solution. The statement is $\forall A\, \bigl( (E(A) \wedge B(A)) \to S(A) \bigr)$ . By Proposition 6.2.1 (a) and (b) and then Proposition 6.2.2, its negation is $\exists A \; \bigl( (E(A) \wedge B(A)) \wedge \neg S(A) \bigr):$ there is a non-empty set of reals, bounded above, with no supremum. The two conditions are not negated: they stay as conditions on the counterexample, just as a bound stays with its quantifier.

Quick check. Negate “ $f$ is bounded on $A$ ”, $\exists M\; \forall x \in A\; (\left| f(x) \right| \le M)$ , into positive form, and say it in words.

Warning. The negation of an implication is not an implication. “If $x > 2$ , then $x^2 > 4$ ” is not negated by “if $x > 2$ , then $x^2 \le 4$ ”, nor by “if $x \le 2$ , then $x^2 \le 4$ ”. For $x = 0$ the original is true (its hypothesis fails), and so is the second candidate, so the candidate cannot be its negation. The negation is $x > 2 \wedge x^2 \le 4$ (Proposition 6.2.2), and it is false for every real $x$ .

6.2.5. Four forms and their square

Four sentence shapes come up so often that they have names. Fix two one-place predicates $S$ and $P$ .

A, “every $S$ is $P$ ”: $\forall x\, (S(x) \to P(x))$ ;
E, “no $S$ is $P$ ”: $\forall x\, (S(x) \to \neg P(x))$ ;
I, “some $S$ is $P$ ”: $\exists x\, (S(x) \wedge P(x))$ ;
O, “some $S$ is not $P$ ”: $\exists x\, (S(x) \wedge \neg P(x))$ .

The diagonals always hold: A and O are each the negation of the other, and so are E and I. The other three labels hold only when something is an $S$ .

The diagonals, by the laws. A–O is the two steps of the proof of Proposition 6.2.3 (a), QN and then NIm under $\exists$ , which work for the bound $S(x)$ as for $\mathrm{Prime}(n)$ above. E–I is the same, followed by Proposition 2.5.1 under $\exists x$ (by Proposition 6.2.4).

Contrary against contradictory. A and E are contrary: never both true when something is an $S$ , but possibly both false. The negation of “every element of $A$ is positive” is the O form “some element of $A$ is not positive”, not the E form “every element of $A$ is non-positive”.

Example (The square for multiples of 4 and squares)

Over $\mathbb{N}$ , let $S$ be “is a multiple of $4$ ” and $P$ “is a perfect square”. Find the truth value of each corner. Then do the same with $S$ read as “is an odd multiple of $4$ ”.

Solution. A, “every multiple of $4$ is a perfect square”, is false at $8$ . E, “no multiple of $4$ is a perfect square”, is false at $4 = 2^2$ . I is true at $4$ , and O at $8$ . Each diagonal joins a true corner to a false one.

No number is an odd multiple of $4$ . Now A and E are both true, vacuously, and I and O both false. Contraries both true, subcontraries both false: this is why the outer labels need something to be an $S$ (existential import, Section 5.1).

Quick check. Which corner is the negation of “no multiple of $4$ is a perfect square”, and is that corner true?

Solution. I: “some multiple of $4$ is a perfect square”. It is true, since $16 = 4 \cdot 4 = 4^2$ . The negation of E is I, by the diagonal.

6.2.6. How the laws look in a mathematical proof

Chapter 2 proved, in Example (A number below every positive number), that a number $x \ge 0$ below every positive number is $0$ . Its key step chose $\varepsilon \mathrel{:=} x/2$ , and the reading after it called “the hypothesis applies to it” a step about “every”, used as ordinary reasoning until Chapter 5. The rule is $\mathrm{\forall E}$ , in its bounded form (Proposition 6.1.1), at a term built from the data. Here is the same move once more, the way it appears in analysis.

Two real numbers that are closer than every positive number are equal.

Proposition 6.2.5 (Arbitrarily Close Numbers Are Equal)

Let $a$ and $b$ be real numbers. If $\left| a - b \right| < \varepsilon$ for every $\varepsilon > 0$ , then $a = b$ .

Idea. The goal $a = b$ is atomic, so no introduction rule applies, and the hypothesis is a $\forall$ whose instances are all inequalities, never an equation. We are stuck, so suppose $a \ne b$ . The hypothesis may be instantiated at any positive term, so choose the term that makes the numbers collide: $\varepsilon \mathrel{:=} \left| a - b \right|$ , which is positive exactly because $a \ne b$ .

Proof. Suppose that $\left| a - b \right| < \varepsilon$ for every $\varepsilon > 0$ , and suppose, for a contradiction, that $a \ne b$ [an $\mathrm{RAA}$ box]. Then $a - b \ne 0$ , so $\left| a - b \right| > 0$ , by the school fact that $\left| u \right| > 0$ for every real $u \ne 0$ . So the hypothesis applies to the term $\left| a - b \right|$ [bounded $\mathrm{\forall E}$ , citing the line $\left| a - b \right| > 0$ ] and gives $\left| a - b \right| < \left| a - b \right|$ . No real number is less than itself, so this is a contradiction [ $\mathrm{\neg E}$ ]. Hence $a = b$ [ $\mathrm{RAA}$ ].

The last step is a genuine $\mathrm{RAA}$ : the box assumed $\neg(a = b)$ , written $a \ne b$ , and concluded $a = b$ ; $\mathrm{\neg I}$ would only have given $\neg\neg(a = b)$ . The hypothesis cannot be weakened to “for some $\varepsilon > 0$ ”: $a = 0$ , $b = \frac12$ , $\varepsilon = 1$ satisfy $\left| a - b \right| < \varepsilon$ and $a \ne b$ . The facts about $\left| \cdot \right|$ used here are school algebra.

Read the result through the negation laws. Its contrapositive says: if $a \ne b$ , then $\neg\forall \varepsilon > 0\, (\left| a - b \right| < \varepsilon)$ , which by Proposition 6.2.3 is interderivable with $\exists \varepsilon > 0\, \neg(\left| a - b \right| < \varepsilon)$ , that is, by the order fact, $\exists \varepsilon > 0\, (\left| a - b \right| \ge \varepsilon)$ . The proof did not search for that $\varepsilon$ : it named it, $\left| a - b \right|$ , from the data. A proof by contradiction in analysis is usually this shape. Negate the goal; the negation hands over an object (here the positive number $\left| a - b \right|$ ); feed it to a hypothesis that holds for every object of its kind.

6.2.7. Moving a quantifier across a connective

Negation is not the only thing that needs moving. A formula such as $\exists x\, P(x) \to \psi$ has its quantifier buried in a hypothesis, and proofs often want it outside, or the reverse. Two groups of laws do this. The distribution laws move a quantifier across $\wedge$ or $\vee$ when both sides mention $x$ ; the passage laws move it across a connective when one side does not. The laws of this subsection are proved by the method’s short runs; the derivations are in a fold, and Section 7.2 returns to two of the one-way laws.

Proposition 6.2.6 (Distribution of Quantifiers)

For all formulas $\varphi$ , $\psi$ and every variable $x$ :

(a) $\forall x\, (\varphi \wedge \psi) \dashv\vdash \forall x\, \varphi \wedge \forall x\, \psi$ ;
(b) $\exists x\, (\varphi \vee \psi) \dashv\vdash \exists x\, \varphi \vee \exists x\, \psi$ ;
(c) $\forall x\, \varphi \vee \forall x\, \psi \vdash \forall x\, (\varphi \vee \psi)$ ;
(d) $\exists x\, (\varphi \wedge \psi) \vdash \exists x\, \varphi \wedge \exists x\, \psi$ .

All four are derived without $\mathrm{RAA}$ .

The proposition collects laws that are mostly proved already. Its point is the comparison: $\forall$ goes across $\wedge$ and $\exists$ across $\vee$ in both directions, while $\forall$ across $\vee$ and $\exists$ across $\wedge$ go one way only.

Idea. Three of the four laws were derived in Sections 5.4 and 5.6 for $P(x)$ and $Q(x)$ ; only the fresh name’s instances were used there, so formulas can take their place. For (c), the goal is a $\forall$ and the premise a disjunction: open the flagged box first, then split on the premise inside it.

The converses of (c) and (d) are false. Over $\mathbb{Z}$ , every integer is even or odd, but neither “every integer is even” nor “every integer is odd” holds; some integer is even and some integer is odd, but none is both. These are counter-readings; Section 7.2 draws them as counter-models.

The passage laws need a condition: the quantified variable must not be free in the formula that the quantifier moves away from. Section 5.2 proved the fact that makes this work: if $x$ is not free in $\psi$ , then $\psi[t/x] = \psi$ for every term $t$ . So an instance of $\psi \to \varphi$ at $x_0$ is $\psi \to \varphi[x_0/x]$ , with $\psi$ untouched.

Proposition 6.2.7 (Passage Laws)

Let $\varphi$ and $\psi$ be formulas and $x$ a variable that is not free in $\psi$ . Then

(a) $\forall x\, (\psi \to \varphi) \dashv\vdash \psi \to \forall x\, \varphi$ ;
(b) $\forall x\, (\varphi \to \psi) \dashv\vdash \exists x\, \varphi \to \psi$ ;
(c) $\exists x\, (\varphi \wedge \psi) \dashv\vdash \exists x\, \varphi \wedge \psi$ ;
(d) $\exists x\, (\varphi \to \psi) \dashv\vdash \forall x\, \varphi \to \psi$ ;
(e) $\exists x\, (\psi \to \varphi) \dashv\vdash \psi \to \exists x\, \varphi$ .

Of the ten directions, two are derived here with $\mathrm{RAA}$ : $\dashv$ in (d), through $\mathrm{LEM}$ and the cited QN (a), and $\dashv$ in (e), through $\mathrm{LEM}$ . The other eight are derived without it.

Read (b) aloud: “everything with $\varphi$ has $\psi$ ” says the same as “if something has $\varphi$ , then $\psi$ ”. In (b) and (d) the quantifier changes from $\forall$ to $\exists$ or back as it leaves the hypothesis of an implication. That is the game reading of Section 5.1 once more: a quantifier in a hypothesis changes sides.

Idea. Each intuitionistic direction is a short run of the search method. A goal $\to$ opens a $\mathrm{{\to}I}$ box; a goal $\forall$ a flagged box; a premise $\exists$ an $\mathrm{\exists E}$ box, early; a premise $\forall$ is instantiated at $x_0$ , where the condition on $\psi$ keeps $\psi$ unchanged; and the $\exists$ goal waits for its witness $x_0$ . The two classical directions get stuck. In (d), the premise $\forall x\, \varphi \to \psi$ is usable only once $\forall x\, \varphi$ is in hand, and it may not be; so decide it, by $\mathrm{LEM}$ . If $\forall x\, \varphi$ holds, then $\psi$ holds, and $\varphi \to \psi$ holds at every $x$ . If not, (a) of Proposition 6.2.1 supplies an $x_0$ with $\neg\varphi[x_0/x]$ , and $\varphi[x_0/x] \to \psi$ is vacuously true. In (e), decide $\psi$ : if $\psi$ holds, the premise supplies a witness; if not, $\psi \to \varphi$ is vacuously true at every $x$ .

Second readingThe derivations of the distribution and passage laws

Proof. For Proposition 6.2.6: (a) is Proposition 5.4.1, (d) is Proposition 5.6.1, and (b) is part (a) of Example (Derivations with existential elimination), the derivation of $\exists$ over $\vee$ . Those derivations are written with $P(x)$ and $Q(x)$ ; they work word for word with $\varphi$ and $\psi$ in their place, because they use nothing about $P(x)$ and $Q(x)$ beyond the instances at the fresh name, which is chosen different from $x$ and not appearing in $\varphi$ or $\psi$ .

For (c), the goal is a $\forall$ : open a flagged box. Inside it the premise is a disjunction, so split on it; in each case one $\mathrm{\forall E}$ at $x_0$ and one $\mathrm{\vee I}$ reach the instance of $\varphi \vee \psi$ :

\forall x\, \varphi \vee \forall x\, \psi

x_0

\forall x\, \varphi

asm, for

\mathrm{{\vee}E}

\varphi[x_0/x]

\mathrm{{\forall}E}

\varphi[x_0/x] \vee \psi[x_0/x]

\mathrm{{\vee}I}

\forall x\, \psi

asm, for

\mathrm{{\vee}E}

\psi[x_0/x]

\mathrm{{\forall}E}

\varphi[x_0/x] \vee \psi[x_0/x]

\mathrm{{\vee}I}

\varphi[x_0/x] \vee \psi[x_0/x]

\mathrm{{\vee}E}

1, 2–4, 5–7

\forall x\, (\varphi \vee \psi)

\mathrm{{\forall}I}

2–8

Line 8 is the instance of $\varphi \vee \psi$ at $x_0$ and the last line of the flagged box; at line 9, $x_0$ is in neither the premise nor the conclusion, and no assumption is open. This proves Proposition 6.2.6.

Proof. In every derivation below, $x_0$ is a variable other than $x$ that does not appear in $\varphi$ or $\psi$ , and $\psi[x_0/x] = \psi$ because $x$ is not free in $\psi$ (Section 5.2). So the instance at $x_0$ of $\psi \to \varphi$ is $\psi \to \varphi[x_0/x]$ , and likewise for the other combinations.

(a), $\vdash$ and $\dashv$ :

\forall x\, (\psi \to \varphi)

\psi

asm, for

\mathrm{{{\to}}I}

x_0

\psi \to \varphi[x_0/x]

\mathrm{{\forall}E}

\varphi[x_0/x]

\mathrm{{{\to}}E}

3, 2

\forall x\, \varphi

\mathrm{{\forall}I}

3–4

\psi \to \forall x\, \varphi

\mathrm{{{\to}}I}

2–5

\psi \to \forall x\, \varphi

x_0

\psi

asm, for

\mathrm{{{\to}}I}

\forall x\, \varphi

\mathrm{{{\to}}E}

1, 2

\varphi[x_0/x]

\mathrm{{\forall}E}

\psi \to \varphi[x_0/x]

\mathrm{{{\to}}I}

2–4

\forall x\, (\psi \to \varphi)

\mathrm{{\forall}I}

2–5

At line 5 on the left the assumption $\psi$ is open, and $x_0$ does not appear in it: this is where the fresh name must avoid $\psi$ .

(b), $\vdash$ and $\dashv$ :

\forall x\, (\varphi \to \psi)

\exists x\, \varphi

asm, for

\mathrm{{{\to}}I}

x_0

\varphi[x_0/x]

asm, for

\mathrm{{\exists}E}

\varphi[x_0/x] \to \psi

\mathrm{{\forall}E}

\psi

\mathrm{{{\to}}E}

4, 3

\psi

\mathrm{{\exists}E}

2, 3–5

\exists x\, \varphi \to \psi

\mathrm{{{\to}}I}

2–6

\exists x\, \varphi \to \psi

x_0

\varphi[x_0/x]

asm, for

\mathrm{{{\to}}I}

\exists x\, \varphi

\mathrm{{\exists}I}

\psi

\mathrm{{{\to}}E}

1, 3

\varphi[x_0/x] \to \psi

\mathrm{{{\to}}I}

2–4

\forall x\, (\varphi \to \psi)

\mathrm{{\forall}I}

2–5

At line 6 on the left, the conclusion $\psi$ does not mention the witness $x_0$ : this is where $\mathrm{\exists E}$ ’s side condition meets the condition on $\psi$ .

(c), $\vdash$ and $\dashv$ :

\exists x\, (\varphi \wedge \psi)

x_0

\varphi[x_0/x] \wedge \psi

asm, for

\mathrm{{\exists}E}

\varphi[x_0/x]

\mathrm{{\wedge}E}

\exists x\, \varphi

\mathrm{{\exists}I}

\psi

\mathrm{{\wedge}E}

\exists x\, \varphi \wedge \psi

\mathrm{{\wedge}I}

4, 5

\exists x\, \varphi \wedge \psi

\mathrm{{\exists}E}

1, 2–6

\exists x\, \varphi \wedge \psi

\exists x\, \varphi

\mathrm{{\wedge}E}

\psi

\mathrm{{\wedge}E}

x_0

\varphi[x_0/x]

asm, for

\mathrm{{\exists}E}

\varphi[x_0/x] \wedge \psi

\mathrm{{\wedge}I}

4, 3

\exists x\, (\varphi \wedge \psi)

\mathrm{{\exists}I}

\exists x\, (\varphi \wedge \psi)

\mathrm{{\exists}E}

2, 4–6

(d), $\vdash$ :

\exists x\, (\varphi \to \psi)

\forall x\, \varphi

asm, for

\mathrm{{{\to}}I}

x_0

\varphi[x_0/x] \to \psi

asm, for

\mathrm{{\exists}E}

\varphi[x_0/x]

\mathrm{{\forall}E}

\psi

\mathrm{{{\to}}E}

3, 4

\psi

\mathrm{{\exists}E}

1, 3–5

\forall x\, \varphi \to \psi

\mathrm{{{\to}}I}

2–6

(d), $\dashv$ , with $\mathrm{LEM}$ on $\forall x\, \varphi$ :

\forall x\, \varphi \to \psi

\forall x\, \varphi \vee \neg \forall x\, \varphi

\mathrm{LEM}

\forall x\, \varphi

asm, for

\mathrm{{\vee}E}

\psi

\mathrm{{{\to}}E}

1, 3

\varphi

asm, for

\mathrm{{{\to}}I}

\psi

\mathrm{R}

\varphi \to \psi

\mathrm{{{\to}}I}

5–6

\exists x\, (\varphi \to \psi)

\mathrm{{\exists}I}

\neg \forall x\, \varphi

asm, for

\mathrm{{\vee}E}

\exists x\, \neg \varphi

QN (a) 9

x_0

\neg \varphi[x_0/x]

asm, for

\mathrm{{\exists}E}

\varphi[x_0/x] \to \psi

VI 11

\exists x\, (\varphi \to \psi)

\mathrm{{\exists}I}

\exists x\, (\varphi \to \psi)

\mathrm{{\exists}E}

10, 11–13

\exists x\, (\varphi \to \psi)

\mathrm{{\vee}E}

2, 3–8, 9–14

Line 8 is $\mathrm{\exists I}$ at the term $x$ itself: $(\varphi \to \psi)[x/x]$ is $\varphi \to \psi$ , as in Proposition 5.5.1, and as there the step is sound because every domain is non-empty (Section 7.1). At line 14, $x_0$ is in neither the conclusion nor line 10, nor in the premise or the open assumption $\neg\forall x\, \varphi$ .

(e), $\vdash$ and $\dashv$ , the second with $\mathrm{LEM}$ on $\psi$ :

\exists x\, (\psi \to \varphi)

\psi

asm, for

\mathrm{{{\to}}I}

x_0

\psi \to \varphi[x_0/x]

asm, for

\mathrm{{\exists}E}

\varphi[x_0/x]

\mathrm{{{\to}}E}

3, 2

\exists x\, \varphi

\mathrm{{\exists}I}

\exists x\, \varphi

\mathrm{{\exists}E}

1, 3–5

\psi \to \exists x\, \varphi

\mathrm{{{\to}}I}

2–6

\psi \to \exists x\, \varphi

\psi \vee \neg \psi

\mathrm{LEM}

\psi

asm, for

\mathrm{{\vee}E}

\exists x\, \varphi

\mathrm{{{\to}}E}

1, 3

x_0

\varphi[x_0/x]

asm, for

\mathrm{{\exists}E}

\psi

asm, for

\mathrm{{{\to}}I}

\varphi[x_0/x]

\mathrm{R}

\psi \to \varphi[x_0/x]

\mathrm{{{\to}}I}

6–7

\exists x\, (\psi \to \varphi)

\mathrm{{\exists}I}

\exists x\, (\psi \to \varphi)

\mathrm{{\exists}E}

4, 5–9

\neg \psi

asm, for

\mathrm{{\vee}E}

\psi \to \varphi

VI 11

\exists x\, (\psi \to \varphi)

\mathrm{{\exists}I}

\exists x\, (\psi \to \varphi)

\mathrm{{\vee}E}

2, 3–10, 11–13

Line 13 is again $\mathrm{\exists I}$ at the variable $x$ . At line 10, $x_0$ is in neither the conclusion $\exists x\, (\psi \to \varphi)$ nor line 4, $\exists x\, \varphi$ , nor in the premise or the open assumption $\psi$ of line 3. In each of the eight other derivations, the side conditions are checked as in Proposition 6.2.1, and $\mathrm{LEM}$ and $\mathrm{RAA}$ do not occur. This proves Proposition 6.2.7.

Why the condition on $\psi$ . Drop it, and (b) fails. Take $\varphi$ and $\psi$ both to be $P(x)$ . Then $\forall x\, (P(x) \to P(x))$ is true in every domain, while $\exists x\, P(x) \to P(x)$ , over $\mathbb{Z}$ with $P$ read as “is even” and $x$ read as $1$ , says “if some integer is even, then $1$ is even”, which is false. The derivation of (b), in the fold above, shows where the condition was used. Without it, line 4 would be $P(x_0) \to P(x_0)$ , line 5 would be $P(x_0)$ , and the $\mathrm{\exists E}$ box could not close on a line that mentions its witness.

Second readingPassage laws on a part

A passage law of Proposition 6.2.7 asks that its moving variable $y$ not be free in $\psi$ ; since $y$ appears in $\beta$ , the fresh $x_0$ is not $y$ . If $y$ is $x$ itself, substitution stops at the quantifier on $x$ , and $\psi[x_0/x]$ is $\psi$ because $x$ is not free in $\psi$ ; the pair is then the law’s own instance, unchanged. Otherwise substituting $x_0$ for $x$ passes the quantifier on $y$ unchanged, and $\psi[x_0/x]$ has no free variable that $\psi$ lacks except $x_0$ , and $y$ is not free in it either. So the pair is again an instance of the law, with its condition met.

Quick check. A student writes $\forall x\, (x > 0 \to \exists y\, (y \cdot y = x))$ as $\forall x\, \exists y\, (x > 0 \to y \cdot y = x)$ , citing a passage law. Which law, and is the condition met?

Solution. Law (e) of Proposition 6.2.7, applied under $\forall x$ (a law may be used on a part under a quantifier: Proposition 6.2.4, with the fold “Passage laws on a part” above), with $\psi$ the formula $x > 0$ , $\varphi$ the formula $y \cdot y = x$ , and $y$ as the moving variable. The condition asks that $y$ not be free in $\psi$ , and $y$ does not occur in $x > 0$ ; so the step is correct. It is the classical direction of (e), the one derived with $\mathrm{LEM}$ .

Second readingTwin laws

Over a domain with two elements $a$ , $b$ , a $\forall$ is an “and” and an $\exists$ is an “or” (Section 5.5 read $\exists$ over a finite domain as a long “or”), and each law of this section becomes a propositional law. Below, $\varphi_a$ abbreviates $\varphi[a/x]$ , the instance at $a$ ; a formula $\psi$ in which $x$ is not free is the same at $a$ and at $b$ .

law	over $\{a, b\}$	the propositional twin
QN (a), (b)	$\neg(\varphi_a \wedge \varphi_b) \dashv\vdash \neg\varphi_a \vee \neg\varphi_b$	Proposition 2.5.5 (d), (c)
QN (c)	$\neg(\varphi_a \vee \varphi_b) \dashv\vdash \neg\varphi_a \wedge \neg\varphi_b$	Proposition 2.5.5 (a), (b)
distribution (c)	$(\varphi_a \wedge \varphi_b) \vee (\psi_a \wedge \psi_b) \vdash (\varphi_a \vee \psi_a) \wedge (\varphi_b \vee \psi_b)$	a direct derivation: $\mathrm{\vee E}$ on the premise, and in each case $\mathrm{\wedge E}$ twice, $\mathrm{\vee I}$ twice and $\mathrm{\wedge I}$
passage (b)	$(\varphi_a \to \psi) \wedge (\varphi_b \to \psi) \dashv\vdash (\varphi_a \vee \varphi_b) \to \psi$	Example (Cases on a hypothesis are two implications), Example (A disjunctive hypothesis splits into two implications)

In each pair the direction that needs $\mathrm{RAA}$ is the same: QN (a) and De Morgan (d). A twin is a reading, not a proof: a domain may be infinite, and the laws were derived for every domain.

6.2.8. Prenex form

A formula is in prenex form when all its quantifiers stand at the front, as a prefix, before a part with no quantifier, the matrix.

Example (Bringing a formula into prenex form)

Bring $\exists x\, P(x) \to \exists y\, Q(y)$ into prenex form.

Solution. $\begin{aligned} &\exists x\, P(x) \to \exists y\, Q(y) \\ \dashv\vdash\; &\forall x\, \bigl( P(x) \to \exists y\, Q(y) \bigr) \\ \dashv\vdash\; &\forall x\, \exists y\, \bigl( P(x) \to Q(y) \bigr). \end{aligned}$

The first step is passage law (b), with $\psi$ the formula $\exists y\, Q(y)$ , in which $x$ is not free.
The second is law (e) under $\forall x$ , by Proposition 6.2.4, with $\psi$ the formula $P(x)$ , in which $y$ is not free. Its hypothesis is checked in the fold “Passage laws on a part”.

Going down, the second step uses the classical direction of (e).

Alternation. Count the changes between $\forall$ and $\exists$ along the prefix: the example has one, $\forall x\, \exists y$ , and “ $a_n \to L$ ” has two, $\forall \varepsilon\; \exists N\; \forall n$ . Each change is one more round of the game of Section 5.1: a challenger move answered by a defender move. A prefix with more alternations takes more rounds to win, and checking it by examples gets harder: no finite table of values settles a $\forall \exists \forall$ sentence over $\mathbb{N}$ .

Quick check. How many alternations have the prefixes of “uniformly continuous on $A$ ” and “continuous at every point of $A$ ” (Section 6.1, Exercise (C1: Where the $\forall x$ stands))?

Solution. Two each: $\forall \varepsilon\; \exists \delta\; \forall x\; \forall y$ and $\forall x\; \forall \varepsilon\; \exists \delta\; \forall y$ . The count is the same, and the order differs. Section 6.4 is about that difference.

Remark (Looking ahead). Chapter 8 says what is at stake when “not every” becomes “some not” by $\mathrm{RAA}$ , and catalogues the wrong negations of this section among the steps a proof may not take.

6.2.9. Exercises

A. Check your understanding

Exercise (A1)

These parts are about the derivation of Proposition 6.2.1 (a).

(a) Which lines are justified by $\mathrm{RAA}$ , and what does each of the two boxes assume and conclude?
(b) Why can the derivation not reach $\exists x\, \neg\varphi$ by one $\mathrm{\exists I}$ directly from the premise?
(c) Line 4 is an $\mathrm{\exists I}$ at $x_0$ . Why is its conclusion not the conclusion of the derivation, although the two formulas are the same?
(d) Run the derivation with $\varphi$ the formula $x \cdot x \ne 2$ , over $\mathbb{R}$ . Write lines 1 and 9 in words. Does any line name the number $\sqrt 2$ ? What more would be needed to reach $\exists x\, (x \cdot x = 2)$ ?
(e) True or false, with a reason: $\exists \varepsilon \le 0\; \neg\varphi$ is a correct way to write the negation of $\forall \varepsilon > 0\; \varphi$ .

Solution. (a) Lines 6 and 9. The inner box (lines 3–5) assumes $\neg\varphi[x_0/x]$ , reaches $\bot$ , and line 6 concludes $\varphi[x_0/x]$ . The outer box (lines 2–8) assumes $\neg\exists x\, \neg\varphi$ , reaches $\bot$ , and line 9 concludes $\exists x\, \neg\varphi$ .

(b) $\mathrm{\exists I}$ needs a line holding an instance $\neg\varphi[t/x]$ . The premise $\neg\forall x\, \varphi$ is not such an instance (its main symbol is $\neg$ followed by $\forall$ ), and no rule takes it apart except $\mathrm{\neg E}$ , which needs $\forall x\, \varphi$ . The premise says a counterexample exists without naming one.

(c) Line 4 lies inside three boxes: the box opened at line 2, and the flagged box of $x_0$ and the inner box, both opened at line 3. It depends on the assumptions on lines 2 and 3, so it is not available at the end. It is used only to clash with line 2. The conclusion on line 9 is reached by closing the outer box with $\mathrm{RAA}$ .

(d) Line 1: “not every real number has a square different from $2$ ”. Line 9: “some real number does not have a square different from $2$ ”, that is, $\exists x\, \neg(x \cdot x \ne 2)$ . No line names $\sqrt 2$ : the only witness on any line is the fresh name $x_0$ , inside boxes that closed, and line 9 comes from $\mathrm{RAA}$ , not from $\mathrm{\exists I}$ . To reach $\exists x\, (x \cdot x = 2)$ , open an $\mathrm{\exists E}$ box on line 9 with the assumption $\neg(x_1 \cdot x_1 \ne 2)$ , apply $\mathrm{\neg\neg E}$ (the formula $x_1 \cdot x_1 \ne 2$ is $\neg(x_1 \cdot x_1 = 2)$ ) to get $x_1 \cdot x_1 = 2$ , and close with $\mathrm{\exists I}$ .

(e) False. By Proposition 6.2.3 the negation is $\exists \varepsilon > 0\; \neg\varphi$ : the bound stays. The wrong form can be true together with the statement it claims to negate. Over $\mathbb{R}$ , take $\varphi$ to be $\varepsilon > 0$ : then $\forall \varepsilon > 0\, (\varepsilon > 0)$ is true, and $\exists \varepsilon \le 0\; \neg(\varepsilon > 0)$ is true as well, with the witness $\varepsilon = 0$ . A statement and its negation are never both true.

Exercise (A2: Drill)

Each part takes a line or two. In (a)–(h), negate the statement into positive form (in (g), choose the negation); the last four parts use the square, the reading over two elements, prenex form and a law under a quantifier.

(a) $\forall x\, P(x)$ .
(b) $\exists x\, (P(x) \wedge Q(x))$ .
(c) $\forall x > 0\; (x^2 > 0)$ , over $\mathbb{R}$ .
(d) “If $n$ is even, then $n^2$ is even”, for one integer $n$ .
(e) $\forall \varepsilon > 0\; \exists \delta > 0\; (\delta < \varepsilon)$ .
(f) $\forall x \in A\; (x \le s)$ .
(g) Which is the negation of $\forall x \in A\; \exists y \in B\; (x < y)$ : (i) $\exists x \in A\; \forall y \in B\; (x \ge y)$ ; (ii) $\exists x \notin A\; \forall y \notin B\; (x \ge y)$ ; (iii) $\forall x \in A\; \exists y \in B\; (x \ge y)$ ?
(h) “ $(a_n)$ is bounded below”: $\exists m\; \forall n \in \mathbb{N}\; (m \le a_n)$ .
(i) Over $\mathbb{N}$ , with $S$ “is a multiple of $3$ ” and $P$ “is odd”, which corner of the square is the negation of “some multiple of $3$ is not odd”, and is it true?
(j) Over $\{a, b\}$ , write $\exists x\, (P(x) \wedge Q(x))$ and $\exists x\, P(x) \wedge \exists x\, Q(x)$ without quantifiers, and give truth values that make the second true and the first false.
(k) Name the passage law, and give a prenex form of $\exists x\, P(x) \to R$ , where $x$ is not free in $R$ .
(l) Is this step correct: from $\forall x\, (P(x) \to Q(x))$ to $\forall x\, (\neg P(x) \to \neg Q(x))$ , “contrapositive under $\forall$ ”?

Solution.

(a) $\exists x\, \neg P(x)$ .
(b) $\forall x\, (\neg P(x) \vee \neg Q(x))$ , equivalently $\forall x\, (P(x) \to \neg Q(x))$ .
(c) $\exists x > 0\; (x^2 \le 0)$ : the bound stays, and the order fact turns $\neg(x^2 > 0)$ into $x^2 \le 0$ .
(d) “ $n$ is even and $n^2$ is not even” (Proposition 6.2.2).
(e) $\exists \varepsilon > 0\; \forall \delta > 0\; (\delta \ge \varepsilon)$ , by the order fact for $\neg(\delta < \varepsilon)$ .
(f) $\exists x \in A\; (x > s)$ .
(g) (i): flip each quantifier, keep each bound.
(h) $\forall m\; \exists n \in \mathbb{N}\; (a_n < m)$ , by the order fact for $\neg(m \le a_n)$ .
(i) A, “every multiple of $3$ is odd”, by the diagonal. It is false: $6$ is a multiple of $3$ and even.
(j) $(P(a) \wedge Q(a)) \vee (P(b) \wedge Q(b))$ and $(P(a) \vee P(b)) \wedge (Q(a) \vee Q(b))$ . Take $P(a)$ and $Q(b)$ true, $P(b)$ and $Q(a)$ false.
(k) Law (b): $\forall x\, (P(x) \to R)$ .
(l) No. The contrapositive is $\forall x\, (\neg Q(x) \to \neg P(x))$ . Over $\mathbb{Z}$ , with $P$ “is a multiple of $4$ ” and $Q$ “is even”, the premise is true and the line is false at $2$ .

B. Practice

Exercise (B1: Four negations)

Negate each definition into positive form, citing the law used at each step. Work over $\mathbb{R}$ , with $(a_n)$ a sequence and $f$ a function.

(a) $(a_n)$ is bounded: $\exists M \; \forall n \in \mathbb{N} \; (\left| a_n \right| \le M)$ .
(b) $f$ is increasing on $A$ : $\forall x \in A \; \forall y \in A \; \bigl( x < y \to f(x) \le f(y) \bigr)$ .
(c) $\lim_{x \to a} f(x) = L$ : $\forall \varepsilon > 0 \; \exists \delta > 0 \; \forall x \; \bigl( (0 < \left| x - a \right| \wedge \left| x - a \right| < \delta) \to \left| f(x) - L \right| < \varepsilon \bigr)$ .
(d) $(a_n)$ is a Cauchy sequence: $\forall \varepsilon > 0 \; \exists N \in \mathbb{N} \; \forall m \in \mathbb{N} \; \forall n \in \mathbb{N} \; \bigl( (m \ge N \wedge n \ge N) \to \left| a_m - a_n \right| < \varepsilon \bigr)$ .

Solution. (a) By Proposition 6.2.1 (c) (the $\exists M$ has no bound), then Proposition 6.2.3 (a) under $\forall M$ : $\neg \exists M \; \forall n \in \mathbb{N} \; (\left| a_n \right| \le M) \dashv\vdash \forall M \; \neg \forall n \in \mathbb{N} \; (\left| a_n \right| \le M) \dashv\vdash \forall M \; \exists n \in \mathbb{N} \; \neg (\left| a_n \right| \le M),$ and the order fact turns $\neg(\left| a_n \right| \le M)$ into $\left| a_n \right| > M$ : $\forall M \; \exists n \in \mathbb{N} \; (\left| a_n \right| > M).$ Every real number is exceeded by the size of some term.

(b) Two uses of Proposition 6.2.3, then Proposition 6.2.2 and the order fact: $\exists x \in A \; \exists y \in A \; \bigl( x < y \wedge f(x) > f(y) \bigr).$ Two points of $A$ , in increasing order, whose values are in decreasing order.

(c) Proposition 6.2.3 twice, Proposition 6.2.1 (a) and (b) for the unbounded $\forall x$ , Proposition 6.2.2, and the order fact: $\exists \varepsilon > 0 \; \forall \delta > 0 \; \exists x \; \bigl( (0 < \left| x - a \right| \wedge \left| x - a \right| < \delta) \wedge \left| f(x) - L \right| \ge \varepsilon \bigr).$ The hypothesis $0 < \left| x - a \right| < \delta$ is not negated: it moves, unchanged, into a conjunction.

(d) Proposition 6.2.3 four times, Proposition 6.2.2, the order fact: $\exists \varepsilon > 0 \; \forall N \in \mathbb{N} \; \exists m \in \mathbb{N} \; \exists n \in \mathbb{N} \; \bigl( (m \ge N \wedge n \ge N) \wedge \left| a_m - a_n \right| \ge \varepsilon \bigr).$ For some $\varepsilon > 0$ , however far out we start, two later terms are at least $\varepsilon$ apart.

Exercise (B2: Two passage laws in one derivation)

Derive $\exists x\, P(x) \to \forall y\, Q(y) \vdash \forall x\, \forall y\, \bigl( P(x) \to Q(y) \bigr)$ without $\mathrm{RAA}$ . Then name the two laws of Proposition 6.2.7 that the sequent combines, and say how.

Solution. The goal is $\forall x$ , then $\forall y$ , then $\to$ : open two flagged boxes and a $\mathrm{{\to}I}$ box, in the goal’s order. Inside, the premise is an implication whose hypothesis $\exists x\, P(x)$ comes from the assumption $P(x_0)$ by $\mathrm{\exists I}$ .

\exists x\, P(x) \to \forall y\, Q(y)

x_0

y_0

P(x_0)

asm, for

\mathrm{{{\to}}I}

\exists x\, P(x)

\mathrm{{\exists}I}

\forall y\, Q(y)

\mathrm{{{\to}}E}

1, 3

Q(y_0)

\mathrm{{\forall}E}

P(x_0) \to Q(y_0)

\mathrm{{{\to}}I}

2–5

\forall y\, (P(x_0) \to Q(y))

\mathrm{{\forall}I}

2–6

\forall x\, \forall y\, (P(x) \to Q(y))

\mathrm{{\forall}I}

2–7

At line 7, $y_0$ is not in the premise or in line 7, and no assumption is open (the box of line 2 has closed). At line 8 the same holds for $x_0$ . No $\mathrm{RAA}$ is used.

The sequent combines (b) and (a) of Proposition 6.2.7. Law (b), with $\varphi$ the formula $P(x)$ and $\psi$ the formula $\forall y\, Q(y)$ (in which $x$ is not free), turns the premise into $\forall x\, \bigl( P(x) \to \forall y\, Q(y) \bigr)$ . Then law (a), applied under $\forall x$ (a provable equivalence may be used under a quantifier, by Proposition 6.2.4) with $\psi$ the formula $P(x)$ , $\varphi$ the formula $Q(y)$ and $y$ as the moving variable ( $y$ is not free in $P(x)$ ), turns $P(x) \to \forall y\, Q(y)$ into $\forall y\, (P(x) \to Q(y))$ .

Exercise (B3: Choosing

\varepsilon

from the data)

Let $a$ and $b$ be real numbers with $a < b + \varepsilon^2$ for every $\varepsilon > 0$ . Prove that $a \le b$ , by the method of Proposition 6.2.5: suppose not, and choose an $\varepsilon$ built from the data that makes the numbers collide. Then explain why the choice $\varepsilon = a - b$ does not work.

Solution. Suppose $a < b + \varepsilon^2$ for every $\varepsilon > 0$ , and suppose, for a contradiction, that $a > b$ (the negation of $a \le b$ ). Let $\varepsilon \mathrel{:=} \min(1, a - b)$ . Then $\varepsilon > 0$ , since $1 > 0$ and $a - b > 0$ . Since $0 < \varepsilon \le 1$ , $\varepsilon^2 = \varepsilon \cdot \varepsilon \le \varepsilon \cdot 1 = \varepsilon$ , and $\varepsilon \le a - b$ . The hypothesis applies to this $\varepsilon$ and gives $a < b + \varepsilon^2 \le b + \varepsilon \le b + (a - b) = a ,$ so $a < a$ , a contradiction. Hence $a \le b$ .

The choice $\varepsilon = a - b$ , copied from the text, gives $a < b + (a - b)^2$ , that is, $a - b < (a - b)^2$ . When $a - b > 1$ this is true (for $a - b = 2$ : $2 < 4$ ), so there is no contradiction. The square shrinks a number only when it is at most $1$ , and the $\min$ with $1$ is what puts $\varepsilon$ there.

Exercise (B4: Derive or break)

Derive each claim with the rules and laws so far, or break it by a reading over $\mathbb{Z}$ that makes every member of its counterexample set true.

(a) $\forall x\, (P(x) \leftrightarrow Q(x)) \vdash \forall x\, P(x) \leftrightarrow \forall x\, Q(x)$ .
(b) $\forall x\, P(x) \leftrightarrow \forall x\, Q(x) \vdash \forall x\, (P(x) \leftrightarrow Q(x))$ .
(c) $\neg\exists x\, (P(x) \wedge \neg Q(x)) \vdash \forall x\, (P(x) \to Q(x))$ .
(d) $\exists x\, P(x) \to \exists x\, Q(x) \vdash \forall x\, (P(x) \to Q(x))$ .
(e) $\forall x\, (P(x) \vee Q(x)) \vdash \forall x\, P(x) \vee \exists x\, Q(x)$ .
(f) $\forall x\, P(x) \vee \exists x\, Q(x) \vdash \forall x\, (P(x) \vee Q(x))$ .

Solution.

(a) Derive. The goal is a biconditional, so $\mathrm{\leftrightarrow I}$ closes two boxes (Definition 2.4.1); in each, the goal is a $\forall$ , so a flagged box.
1 $\forall x\, (P(x) \leftrightarrow Q(x))$
2 $\forall x\, P(x)$ asm, for $\mathrm{{{\leftrightarrow}}I}$
3 $x_0$ $P(x_0) \leftrightarrow Q(x_0)$ $\mathrm{{\forall}E}$ 1
4 $P(x_0)$ $\mathrm{{\forall}E}$ 2
5 $Q(x_0)$ $\mathrm{{{\leftrightarrow}}E}$ 3, 4
6 $\forall x\, Q(x)$ $\mathrm{{\forall}I}$ 3–5
7 $\forall x\, Q(x)$ asm, for $\mathrm{{{\leftrightarrow}}I}$
8 $x_1$ $P(x_1) \leftrightarrow Q(x_1)$ $\mathrm{{\forall}E}$ 1
9 $Q(x_1)$ $\mathrm{{\forall}E}$ 7
10 $P(x_1)$ $\mathrm{{{\leftrightarrow}}E}$ 8, 9
11 $\forall x\, P(x)$ $\mathrm{{\forall}I}$ 8–10
12 $\forall x\, P(x) \leftrightarrow \forall x\, Q(x)$ $\mathrm{{{\leftrightarrow}}I}$ 2–6, 7–11

At line 6, $x_0$ is in neither the premise, the open assumption on line 2, nor $\forall x\, Q(x)$ ; line 11 is checked the same way for $x_1$ .
(b) Breaks. Under the reading with $P$ “is even” and $Q$ “is odd”, every member of the counterexample set is true. Both $\forall x\, P(x)$ and $\forall x\, Q(x)$ are false, so the premise is true; at $0$ , “ $0$ is even if and only if $0$ is odd” is false, so the negated conclusion is true.
(c) Derive. Turn the premise into a $\forall$ by QN (c), then open a flagged box for the goal.

1 $\neg \exists x\, (P(x) \wedge \neg Q(x))$
2 $\forall x\, \neg (P(x) \wedge \neg Q(x))$ QN (c) 1
3 $x_0$ $\neg (P(x_0) \wedge \neg Q(x_0))$ $\mathrm{{\forall}E}$ 2
4 $P(x_0)$ asm, for $\mathrm{{{\to}}I}$
5 $\neg Q(x_0)$ asm, for $\mathrm{RAA}$
6 $P(x_0) \wedge \neg Q(x_0)$ $\mathrm{{\wedge}I}$ 4, 5
7 $\bot$ $\mathrm{{\neg}E}$ 6, 3
8 $Q(x_0)$ $\mathrm{RAA}$ 5–7
9 $P(x_0) \to Q(x_0)$ $\mathrm{{{\to}}I}$ 4–8
10 $\forall x\, (P(x) \to Q(x))$ $\mathrm{{\forall}I}$ 3–9

At line 10, $x_0$ is in neither the premise nor the conclusion, and no assumption is open.
(d) Breaks. Under the reading with $P$ “is even” and $Q$ “is positive”, every member of the counterexample set is true. Some integer is even ( $2$ ) and some integer is positive ( $1$ ), so the premise is true; “every even integer is positive” fails at $0$ , so the negated conclusion is true.
(e) Derive. Decide $\forall x\, P(x)$ by $\mathrm{LEM}$ ; in the second case QN (a) supplies a witness that fails $P$ , and the premise gives it $Q$ .

1 $\forall x\, (P(x) \vee Q(x))$
2 $\forall x\, P(x) \vee \neg \forall x\, P(x)$ $\mathrm{LEM}$
3 $\forall x\, P(x)$ asm, for $\mathrm{{\vee}E}$
4 $\forall x\, P(x) \vee \exists x\, Q(x)$ $\mathrm{{\vee}I}$ 3
5 $\neg \forall x\, P(x)$ asm, for $\mathrm{{\vee}E}$
6 $\exists x\, \neg P(x)$ QN (a) 5
7 $x_0$ $\neg P(x_0)$ asm, for $\mathrm{{\exists}E}$
8 $P(x_0) \vee Q(x_0)$ $\mathrm{{\forall}E}$ 1
9 $Q(x_0)$ $\mathrm{DS}$ 8, 7
10 $\exists x\, Q(x)$ $\mathrm{{\exists}I}$ 9
11 $\exists x\, Q(x)$ $\mathrm{{\exists}E}$ 6, 7–10
12 $\forall x\, P(x) \vee \exists x\, Q(x)$ $\mathrm{{\vee}I}$ 11
13 $\forall x\, P(x) \vee \exists x\, Q(x)$ $\mathrm{{\vee}E}$ 2, 3–4, 5–12

At line 11, $x_0$ is not in line 11, in line 6, in the premise or in the open assumption on line 5.
(f) Breaks. Under the reading with $P$ “is even” and $Q(x)$ “ $x = 0$ ”, every member of the counterexample set is true. Some integer is $0$ , so $\exists x\, Q(x)$ and the premise are true; “every integer is even or equal to $0$ ” fails at $1$ , so the negated conclusion is true.
(g) and (b), and (e) and (f), are converse pairs; (d) asks for more than its premise gives. The breaks are counter-readings (Section 7.2).

Marking scheme. (10 points)

6: one for each correct verdict.
2: the derivations of (a), (c) and (e), with the side condition checked at every closing line of a flagged or $\mathrm{\exists E}$ box.
2: the three readings, each with the truth values of the premise and of the conclusion justified.

Fatal errors (0 for the part): a “break” whose reading leaves the premise false; a derivation that closes an $\mathrm{\exists E}$ box on a line that mentions its witness.

Exercise (B5: Find the error)

Here is a “derivation” of $\exists x\, (P(x) \wedge Q(x)), \ \forall x\, (Q(x) \to R(x)) \vdash \exists x\, R(x)$ .

\exists x\, (P(x) \wedge Q(x))

\forall x\, (Q(x) \to R(x))

P(c) \wedge Q(c)

\mathrm{{\exists}E}

Q(c)

\mathrm{{\wedge}E}

Q(c) \to R(c)

\mathrm{{\forall}E}

R(c)

\mathrm{{{\to}}E}

5, 4

\exists x\, R(x)

\mathrm{{\exists}I}

Is the conclusion derivable? Does this derivation prove it? Find the line that fails, break the step that line takes, and repair the derivation.

Solution. The conclusion is derivable, and this derivation does not prove it. Line 3 fails: $\mathrm{\exists E}$ is not a one-line step. It opens a box whose witness is a fresh variable, never a constant (a constant has a fixed meaning), and the box must close on a line that does not mention the witness; here no box is opened. Nothing licenses passing from “something has $P$ and $Q$ ” to “ $c$ has them”.

The step from $\exists x\, (P(x) \wedge Q(x))$ to $P(c) \wedge Q(c)$ breaks over $\mathbb{Z}$ , with $P$ “is even”, $Q$ “is positive” and $c$ read as $0$ : the premise is true ( $2$ is both), and the line is false, since $0$ is not positive.

The repair opens an $\mathrm{\exists E}$ box:

\exists x\, (P(x) \wedge Q(x))

\forall x\, (Q(x) \to R(x))

x_0

P(x_0) \wedge Q(x_0)

asm, for

\mathrm{{\exists}E}

Q(x_0)

\mathrm{{\wedge}E}

Q(x_0) \to R(x_0)

\mathrm{{\forall}E}

R(x_0)

\mathrm{{{\to}}E}

5, 4

\exists x\, R(x)

\mathrm{{\exists}I}

\exists x\, R(x)

\mathrm{{\exists}E}

1, 3–7

At line 8, $x_0$ is not in line 8, in line 1 or in a premise, and no other assumption is open.

Marking scheme. (10 points)

2: “derivable, but not proved by this derivation”.
3: line 3, and the rule it breaks: $\mathrm{\exists E}$ needs a box with a fresh witness.
2: a reading that breaks the step, with both truth values.
3: a repaired derivation, with the side condition of $\mathrm{\exists E}$ checked.

Fatal error (0 for the step): naming line 7 ( $\mathrm{\exists I}$ is legal there).

C. Going deeper

Exercise (C1: Two prenex forms)

A formula is in prenex form when all its quantifiers stand at the front, before a part with no quantifier. Using the laws of Proposition 6.2.7, bring $\forall x\, P(x) \to \exists y\, Q(y)$ into prenex form in two ways, ending with $\exists x\, \exists y\, (P(x) \to Q(y))$ and with $\exists y\, \exists x\, (P(x) \to Q(y))$ . Justify each step, and say which directions of the laws are classical.

Solution (Hint 1). The formula is an implication with a quantifier on each side. Law (d) moves the quantifier out of the hypothesis, and law (e) moves it out of the conclusion.

Solution (Hint 2). For the first route, start with law (d), taking $\psi$ to be the whole conclusion $\exists y\, Q(y)$ .

Solution. First route: $x$ out first. Law (d) of Proposition 6.2.7, with $\varphi$ the formula $P(x)$ and $\psi$ the formula $\exists y\, Q(y)$ , in which $x$ is not free: $\forall x\, P(x) \to \exists y\, Q(y) \;\dashv\vdash\; \exists x\, \bigl( P(x) \to \exists y\, Q(y) \bigr).$ Then law (e) under $\exists x$ , with $\psi$ the formula $P(x)$ , $\varphi$ the formula $Q(y)$ , and $y$ as the moving variable ( $y$ is not free in $P(x)$ ): $P(x) \to \exists y\, Q(y) \dashv\vdash \exists y\, (P(x) \to Q(y))$ . A provable equivalence may be used under a quantifier (Proposition 6.2.4), so $\exists x\, \bigl( P(x) \to \exists y\, Q(y) \bigr) \;\dashv\vdash\; \exists x\, \exists y\, \bigl( P(x) \to Q(y) \bigr).$

Second route: $y$ out first. Law (e), with $\psi$ the formula $\forall x\, P(x)$ , $\varphi$ the formula $Q(y)$ , and $y$ as the moving variable ( $y$ is not free in $\forall x\, P(x)$ ): $\forall x\, P(x) \to \exists y\, Q(y) \;\dashv\vdash\; \exists y\, \bigl( \forall x\, P(x) \to Q(y) \bigr).$ Then law (d) under $\exists y$ , with $\varphi$ the formula $P(x)$ and $\psi$ the formula $Q(y)$ ( $x$ is not free in $Q(y)$ ): $\exists y\, \bigl( \forall x\, P(x) \to Q(y) \bigr) \;\dashv\vdash\; \exists y\, \exists x\, \bigl( P(x) \to Q(y) \bigr).$

Classical steps. Going from the given formula towards the prenex form, every step of both routes uses the direction $\dashv$ of (d) or of (e): the direction from the implication to the $\exists$ . These are exactly the two directions that Proposition 6.2.7 derives with $\mathrm{LEM}$ . The way back uses only the intuitionistic directions.

Marking scheme. (10 points) - 3: first route, with law (d) then law (e), each with $\varphi$ , $\psi$ and the moving variable named, and the “not free” condition checked. - 3: second route, likewise with (e) then (d). - 2: says why a law may be applied under $\exists x$ or $\exists y$ (an equivalence used under a quantifier, by an $\mathrm{\exists E}$ box closed with $\mathrm{\exists I}$ ). - 2: identifies the $\dashv$ directions of (d) and (e) as the classical ones, used in every step towards prenex form. Fatal errors (0 for the step): moving $\forall x$ out of the hypothesis as $\forall x$ (it becomes $\exists x$ ); applying a passage law when the moving variable is free in $\psi$ .

Exercise (C2: Exit check: negations)

(a) A sequence of functions $f_n$ converges to $f$ uniformly on $A$ when $\forall \varepsilon > 0 \; \exists N \in \mathbb{N} \; \forall n \in \mathbb{N} \; \forall x \in A \; \bigl( n \ge N \to \left| f_n(x) - f(x) \right| < \varepsilon \bigr),$ where $f_n(x)$ is a term in the two variables $n$ and $x$ . Negate this into positive form, citing the laws.
(b) Using the negation of uniform continuity in Example (Three negations from analysis) (c), prove that $f(x) = 1/x$ is not uniformly continuous on $(0, 1)$ . Give the witnesses that the negation asks for, each as a function of what is chosen before it, and check every condition.

Solution (Hint 1). For (b), the negation asks for one $\varepsilon$ first. Near $0$ , the graph of $1/x$ is steep: two points close together have values far apart.

Solution (Hint 2). Take $\varepsilon = 1$ and let $\delta > 0$ be arbitrary. You must now find $x, y \in (0, 1)$ , depending on $\delta$ , with $\left| x - y \right| < \delta$ and $\left| 1/x - 1/y \right| \ge 1$ .

Solution. (a) Proposition 6.2.3 four times, then Proposition 6.2.2 and the order fact: $\exists \varepsilon > 0 \; \forall N \in \mathbb{N} \; \exists n \in \mathbb{N} \; \exists x \in A \; \bigl( n \ge N \wedge \left| f_n(x) - f(x) \right| \ge \varepsilon \bigr).$ In words: for some $\varepsilon > 0$ , however far out we start, some later $f_n$ is at least $\varepsilon$ away from $f$ at some point of $A$ . The point may change with $n$ .

(b) By Example (Three negations from analysis) (c), we must prove $\exists \varepsilon > 0 \; \forall \delta > 0 \; \exists x \in (0, 1) \; \exists y \in (0, 1) \; \Bigl( \left| x - y \right| < \delta \wedge \Bigl\lvert \frac1x - \frac1y \Bigr\rvert \ge \varepsilon \Bigr).$ Take $\varepsilon = 1$ , which is positive. Let $\delta > 0$ be arbitrary, and let $t \mathrel{:=} \min(\delta, \tfrac12)$ , so $0 < t \le \tfrac12$ and $t \le \delta$ ; then take $x \mathrel{:=} t$ and $y \mathrel{:=} t/2$ , which depend on $\delta$ . Check:

$x, y \in (0, 1)$ : $0 < t/2 < t \le \tfrac12 < 1$ .
$\left| x - y \right| = t/2 < t \le \delta$ , since $t > 0$ .
$\left| 1/x - 1/y \right| = \left| 1/t - 2/t \right| = 1/t \ge 2 \ge 1 = \varepsilon$ , since $t \le \tfrac12$ .

Since $\delta > 0$ was arbitrary, the negation of uniform continuity holds, so $1/x$ is not uniformly continuous on $(0, 1)$ .

Marking scheme. (10 points) - 3: (a) the negation, with every bound kept, $\wedge$ in place of $\to$ , and the quantifiers in the order $\exists \varepsilon\; \forall N\; \exists n\; \exists x \in A$ . - 2: (b) the witness $\varepsilon$ , stated before $\delta$ is given. - 2: for an arbitrary $\delta > 0$ , points $x$ and $y$ given as functions of $\delta$ . - 3: the three checks: $x, y \in (0, 1)$ ; $\left| x - y \right| < \delta$ ; $\left| f(x) - f(y) \right| \ge \varepsilon$ . A different correct choice earns full marks (for instance $x = t$ , $y = t/3$ ); the scheme rewards the order of the choices and the checks. Fatal errors (0 for the step): $\varepsilon$ chosen depending on $\delta$ ; points chosen before $\delta$ is given, or not depending on it where they must; a bound negated instead of the quantifier ( $\exists \varepsilon \le 0$ , $\exists n < N$ ).

Exercise (C3: “There exists” from “for every”)

Suppose $\exists$ were not a symbol of the language, and $\exists x\, \varphi$ abbreviated $\neg\forall x\, \neg\varphi$ .

(a) Show that $\mathrm{\exists I}$ is then a derived step: from $\varphi[t/x]$ , with $t$ free for $x$ in $\varphi$ , derive $\neg\forall x\, \neg\varphi$ .
(b) Show that $\mathrm{\exists E}$ is one too: if $\Gamma, \varphi[x_0/x] \vdash \chi$ , where $x_0$ is a variable other than $x$ that appears neither in $\Gamma$ , nor in $\chi$ , nor in $\varphi$ , then $\Gamma, \neg\forall x\, \neg\varphi \vdash \chi$ .
(c) Which of (a) and (b) uses a classical rule ( $\mathrm{RAA}$ or $\mathrm{LEM}$ )?

Solution (Hint 1). In (a) the goal is a negation: open a $\mathrm{\neg I}$ box.

Solution (Hint 2). In (b) nothing in the premises can be taken apart; aim the clash at the premise $\neg\forall x\, \neg\varphi$ .

Solution. (a) Five lines:

\varphi[t/x]

\forall x\, \neg \varphi

asm, for

\mathrm{{\neg}I}

\neg \varphi[t/x]

\mathrm{{\forall}E}

\bot

\mathrm{{\neg}E}

1, 3

\neg \forall x\, \neg \varphi

\mathrm{{\neg}I}

2–4

Line 3 is $\mathrm{\forall E}$ at $t$ , which is free for $x$ in $\neg\varphi$ because it is free for $x$ in $\varphi$ .

(b) From the premises $\Gamma$ and $\neg\forall x\, \neg\varphi$ :

assume $\neg\chi$ , for $\mathrm{RAA}$ ;
open a flagged box $x_0$ , and in it assume $\varphi[x_0/x]$ , for $\mathrm{\neg I}$ ;
paste the given derivation of $\chi$ , whose premises $\Gamma$ are available. Its own flags are first renamed to names that appear nowhere else, as “The laws as one line” requires, so that the open assumption $\neg\chi$ cannot spoil its side conditions;
write $\bot$ by $\mathrm{\neg E}$ with $\neg\chi$ , and $\neg\varphi[x_0/x]$ by $\mathrm{\neg I}$ ; close the flagged box with $\forall x\, \neg\varphi$ by $\mathrm{\forall I}$ . Here $x_0$ is in no premise, not in the open assumption $\neg\chi$ and not in $\forall x\, \neg\varphi$ ;
write $\bot$ by $\mathrm{\neg E}$ with the premise $\neg\forall x\, \neg\varphi$ , and $\chi$ by $\mathrm{RAA}$ .

(c) (b) uses one: $\mathrm{RAA}$ at its last line (or $\mathrm{LEM}$ , in a proof by cases); (a) uses neither. (Whether (b) could avoid a classical rule altogether is not asked.)

Marking scheme. (10 points)

3: (a).
2: (b)’s classical step ( $\mathrm{RAA}$ , or $\mathrm{LEM}$ with a case split) and flagged box, in the right nesting.
3: the side condition of the $\mathrm{\forall I}$ line, including the renaming of the pasted flags.
2: (c).

Fatal errors (0 for the step): $\mathrm{\forall I}$ on $x_0$ while $\varphi[x_0/x]$ is still open; instantiating $\neg\forall x\, \neg\varphi$ by $\mathrm{\forall E}$ .