5.6  Using “There Exists”: Name a Witness

Section 5.5 gave the rule that proves an existential statement: exhibit a witness, and forget it. This section gives the rule that uses one, $\mathrm{\exists }\mathrm{E}$. It is the last of the four quantifier rules, and the subtlest, because an existential says that a witness exists without saying which one it is. The rule handles this with a box and a fresh name, as $\mathrm{\forall }\mathrm{I}$ did, but the name now stands for an object that is not arbitrary, and the side condition keeps it from being treated as if it were. With the rule in hand, the section moves an $\mathrm{\exists }$ past a $\mathrm{\forall }$, and shows exactly where the reverse move breaks down.

5.6.1. Using a witness whose identity is unknown

Chapter 2 proved that if $n^2$ is even then $n$ is even (Theorem 2.1.3). One of the facts it rested on, (E3), says that the square of an odd integer is odd, and it was shown by taking “an integer $k$ with $n=2k+1$” and computing with it. Chapter 2 noted that naming the $k$ of (E3) lay outside its derivation: it is a quantifier step, whose rule had to wait. Here is the simplest proof with the same step.

If $n$ is even, then $n+2$ is even. Since $n$ is even, choose an integer $k$ with $n=2k$. Then $n+2=2k+2=2(k+1)$, so $n+2$ is even.

The hypothesis is $\mathrm{\exists }k(n=2\cdot k)$. The proof does not know which integer $k$ is; it does not need to. It gives the unknown witness a name, uses the one fact it has about it, $n=2k$, and reaches a conclusion, “$n+2$ is even”, in which the name no longer appears. The witness $k+1$ of the last step is forgotten by $\mathrm{\exists }\mathrm{I}$, as in Section 5.5.

Why is this correct? Two tempting shortcuts show what the proof is careful not to do.

• It does not name the witness by a term that already means something. From “some integer is even” we may not conclude “$3$ is even”: the existential does not say that the witness is $3$, and, as the warning “$\mathrm{\exists }\mathrm{I}$ runs one way only” of Section 5.5 noted, it cannot be read back as a statement about a named object.
• It does not let the conclusion mention the name. If it did, the conclusion would be a statement about $k$, and outside the argument $k$ refers to nothing; the existential promised only that some $k$ works.

So the name must be new, the argument may use only what the existential says about it, and the conclusion must not mention it. Then the argument works for the witness, whichever integer it is, because it never used anything else about it.

5.6.2. The rule of existential elimination

To use “there exists”, give the witness a new name, assume only what the existential says about it, and conclude something that does not mention it.

The box of $\mathrm{\exists }\mathrm{E}$ is the flagged box of Section 5.4 with one difference: it opens with an assumption, $\phi [x_0/x]$, “$x_0$ is a witness”. The flagged box of $\mathrm{\forall }\mathrm{I}$ had no assumption, because “let $x_0$ be arbitrary” assumes nothing about $x_0$. The citation “$\mathrm{\exists }\mathrm{E}$ $h$, $i$–$j$” names the line of the existential and the box, as $\vee \mathrm{E}$ names its disjunction and its boxes. “Appear” is the word of Section 5.2: written anywhere in the formula, after a quantifier symbol included. In a finished derivation the box’s assumption is printed “asm, for $\mathrm{\exists }\mathrm{E}$”; read it as “choose $x_0$ with …”.

In practice, two habits make every clause of the side condition hold: name the witness with a brand-new letter, written nowhere in the derivation so far, and make sure the box’s last line does not mention it. Clauses 3–5 below, the side condition, are the official test, the one a checker runs.

This rule has conditions that matter; read each one.

1. The assumption. The box assumes $\phi [x_0/x]$: the formula of the existential, with the new name in place of $x$. This is “choose $x_0$ with $\phi$”. It is the only thing the box knows about $x_0$.
2. The last line. The box ends with $\chi$, a line of the box itself, not of a box inside it, as for $\vee \mathrm{E}$ and $\mathrm{\forall }\mathrm{I}$. It is “whatever the witness is, $\chi$ follows”. The new line $k$ then asserts $\chi$ outside the box, where $x_0$ is no longer assumed to be anything.
3. $x_0$ does not appear in $\chi$. The box shows that $\chi$ follows from “$x_0$ is a witness”; if $\chi$ mentioned $x_0$, line $k$ would make a claim about a name that, outside the box, is tied to nothing. The subsection “Three ways to break the rule” below shows the damage.
4. $x_0$ does not appear in a premise or in an assumption of an open box. The name must be new to everything we know at line $k$. If a premise or an open assumption already said something about $x_0$, the assumption $\phi [x_0/x]$ would add to it a claim that $x_0$ is the witness, which the existential never made.
5. $x_0$ does not appear in $\mathrm{\exists }x\phi$. The existential must not itself mention the name chosen for its witness. This clause also makes $x_0$ free for $x$ in $\phi$ (Section 5.2: a variable that does not appear in $\phi$ is free for every variable there), so the assumption $\phi [x_0/x]$ says of $x_0$ exactly what $\phi$ says of $x$.
6. “Still open at line $k$”. The box’s own assumption $\phi [x_0/x]$ is closed at line $k$, so it is not among the assumptions checked. This matters: read inside the box, “an open assumption” would include $\phi [x_0/x]$, which contains $x_0$ whenever $x$ is free in $\phi$, and the rule could then never be applied in the cases that matter.

A first witness: $n+2$ is even

Here is the proof above as a derivation, over $\mathbb{Z}$, with “$n$ is even” written $\mathrm{\exists }k(n=2\cdot k)$ and the computation as one line justified “arith” (Section 5.3). The premise is an existential, so its box opens first, aimed at the goal (left); the goal is postponed until a line shows its witness (right).

At line 5, $k_0$ is not in line 4, not in the existential of line 1, which is also the only premise, and no box is open. The derivation and the proof match sentence for sentence:

One box instead of many cases

The long “or” of Section 5.1 shows why the rule has this shape. Over a domain whose elements are named $m$ and $n$, $\mathrm{\exists }xP(x)$ says $P(m)\vee P(n)$, and $\vee \mathrm{E}$ (Definition 1.6.1) would use it by proving the goal twice, once in each case. The cases look alike, so they can be done once, with a name that could be either.

On the left, Section 1.6’s rule over the two named elements; on the right, the same argument by $\mathrm{\exists }\mathrm{E}$. Each case box on the left is the box on the right with $m$ or $n$ in place of $x_0$. Because $x_0$ is fresh, one box serves for every element, named or not, and for domains that cannot be listed.

5.6.3. Using an existential: open the box early

When a resource is $\mathrm{\exists }x\phi$, the premise-directed step of the search method is to open its $\mathrm{\exists }\mathrm{E}$ box at once, with a fresh name $x_0$, and to make the box’s last line the current goal. Inside the box, the assumption $\phi [x_0/x]$ is a new resource, and the name $x_0$ is a new term for later steps to use.

Name the witness early: open the $\mathrm{\exists }\mathrm{E}$ box as soon as the existential is available, and aim it at the current goal.

Why early? Opening early keeps every resource, since every line available before the box is available inside it; and a box aimed at the current goal can always be closed once the goal is reached, since its name was chosen fresh. What the early box gives is the witness’s name, often exactly the term a postponed $\mathrm{\exists }$ goal is waiting for.

The first result is the derivation that this step writes almost by itself.

Notice where the witness went. It was used twice inside the box, as the witness of two different existentials, and then forgotten twice. The conclusion records that something has $P$ and something has $Q$, and no longer that it is the same thing.

5.6.4. Three ways to break the rule

Each of clauses 3, 4 and 5 can be seen failing, and each failure leads from premises that are true, under the reading given, to a false line. Here is clause 3, beside a correct use of the same premise; the fold after it breaks clauses 4 and 5.

The conclusion clause (3). Over $\mathbb{N}$, “some number exceeds $5$” is true. Let the $\mathrm{\exists }\mathrm{E}$ box end in the line $x_0>5$, which mentions its own witness:

Line 3 breaks clause 3. Every other line is legal: in particular line 5 is a correct $\mathrm{\forall }\mathrm{I}$, since $x_0$ appears in no premise and in no open assumption (there is none), and not in line 5. Over $\mathbb{N}$ the conclusion says that every number exceeds $5$, which is false at $0$. Once the name leaves its box, it can be generalized over as if it were arbitrary.

On the right, a correct use of the same premise: the box ends in $\mathrm{\exists }x(x>6)$, which forgets the witness before the box closes, and the conclusion is true over $\mathbb{N}$.

A small world in which the premise is true and the line that breaks clause 3 is false. The label “$>5$” is the one-place predicate $x>5$ ($5$ is not a dot); the dashed arrow gives $x_0$ the value $0$. The premise is true (at $6$); line 3, $x_0>5$, is false; so is line 5 (at $0$).

↺Second readingClauses 4 and 5, broken

The premise clause (4). Over $\mathbb{N}$, with $P$ read as “even” and the variable $x_0$ read as $1$, both premises below are true: some number is even, and $1$ is not even.

1$\mathrm{\exists }xP(x)$

2$\mathrm{\neg }P(x_0)$

3$x_0$$P(x_0)$asm, for $\mathrm{\exists }\mathrm{E}$

4$\mathrm{\perp }$$\mathrm{\neg }\mathrm{E}$ 3, 2

5$\mathrm{\perp }$$\mathrm{\exists }\mathrm{E}$ 1, 3–4

Line 5 breaks clause 4: $x_0$ appears in the premise on line 2. The box assumed that $x_0$, which the premise had already described as odd, is the even witness, and derived a contradiction from that assumption, not from the premises.

The existential clause (5). Over $\mathbb{Z}$, with $R(x,y)$ read as “$x<y$”, the premise below says that every integer has a smaller one: true.

1$\mathrm{\forall }y\mathrm{\exists }xR(x,y)$

2$\mathrm{\exists }xR(x,x_0)$$\mathrm{\forall }\mathrm{E}$ 1

3$x_0$$R(x_0,x_0)$asm, for $\mathrm{\exists }\mathrm{E}$

4$\mathrm{\exists }zR(z,z)$$\mathrm{\exists }\mathrm{I}$ 3

5$\mathrm{\exists }zR(z,z)$$\mathrm{\exists }\mathrm{E}$ 2, 3–4

Line 2 is a legal $\mathrm{\forall }\mathrm{E}$ at the term $x_0$. Line 5 breaks clause 5: the existential on line 2 is $\mathrm{\exists }x\phi$ with $\phi =R(x,x_0)$, and $x_0$ appears in it. The assumption $\phi [x_0/x]$ on line 3 is $R(x_0,x_0)$: the box has assumed that the witness smaller than $x_0$ is $x_0$ itself. The conclusion says that some integer is less than itself, which is false. The other clauses hold at line 5: $x_0$ is not in $\mathrm{\exists }zR(z,z)$, not in the premise, and no box is open.

Two small worlds, one per clause: in each, the premises are true and the line that breaks the clause is false. Left, clause 4: the dots $1$ and $2$, with $P$ (“even”) true at $2$ only, and $x_0$ naming $1$; both premises, $\mathrm{\exists }xP(x)$ and $\mathrm{\neg }P(x_0)$, are true, and the line $\mathrm{\perp }$ is false, as always. Right, clause 5: three dots, an arrow from $u$ to $v$ meaning $R(u,v)$; the premise $\mathrm{\forall }y\mathrm{\exists }xR(x,y)$ is true, since every dot has an arrow into it, and the line $\mathrm{\exists }zR(z,z)$ is false, since there is no loop.

A fourth illegal pattern, a second witness given a name that an open assumption already uses, is the error of the warning “Two witnesses, one name” below.

Here are three more derivations, each with an Idea saying why each rule was chosen: two for part (a), one for each direction, and one for part (b).

5.6.5. Moving one quantifier past another

Section 5.1 read $\mathrm{\exists }y\mathrm{\forall }x\phi$ and $\mathrm{\forall }x\mathrm{\exists }y\phi$ as games, and observed that the first gives the second: if one $y$ works for every $x$, then for every $x$ some $y$ works, namely the same one. Here is that observation as a derivation, with the letters of a two-place predicate. It shows, written out in full, a pattern that later derivations of the chapter use again and again and that later exercises leave more and more of to the reader.