5.8 Unique Existence, Counting and Descriptions

Mathematics says “the limit”, “the maximum”, “the inverse”, and it defines new words all the time: “we define $\left| x \right|$ to be …”, “call $n$ even if …”. This section is about the logic behind both habits. It starts with “there is exactly one”, which licenses “the”. Then it counts with equality, turns “the $x$ such that $\varphi$ ” into a name that may be used only after uniqueness is proved, and sets a function symbol beside its graph. Last, it shows why introducing a new symbol by a definition never proves anything new about the old ones. No new rule is needed: equality and the quantifiers do all the work.

5.8.1. Unique existence

Mathematics says “the limit of the sequence”, “the supremum of $A$ ”, “the additive inverse of $a$ ”. Each “the” makes two claims. There is such an object, and there is only one, so that the name picks it out. The second claim is the one that is easy to forget, and the one the claim at the start of Section 5.7 was about.

“There is exactly one $x$ with $\varphi$ ”: there is one, and any other is it.

Definition 5.8.1 (Unique Existence)

Let $\varphi$ be a formula, $x$ a variable, and $y$ a variable other than $x$ that does not appear in $\varphi$ (Section 5.2). Then $\exists! x\, \varphi \quad \text{abbreviates} \quad \exists x\, \bigl( \varphi \wedge \forall y\, (\varphi[y/x] \to y = x) \bigr).$ We read $\exists! x\, \varphi$ as “there is exactly one $x$ such that $\varphi$ ”, or “there is a unique $x$ with $\varphi$ ”.

In words: there is an $x$ that satisfies $\varphi$ , and every $y$ that satisfies $\varphi$ (that is, satisfies $\varphi$ with $y$ in place of $x$ ) is equal to that $x$ . The first conjunct is existence. The second is uniqueness, and it is a statement about the $x$ already found: any other candidate coincides with it. Like the bounded quantifiers of Definition 5.1.1, $\exists!$ is not a new symbol of the language but shorthand, and every rule applies to the formula it abbreviates.

Well-definedness. The abbreviation does not depend on the choice of $y$ , up to renaming a bound variable. The argument, in the fold below, rests on one fact about substitution that the proof of Proposition 5.8.1 uses again: if $y$ does not appear in $\varphi$ , then $(\varphi[y/x])[t/y]$ is $\varphi[t/x]$ .

Second readingWell-definedness, proved

This is a structural induction on $\varphi$ of the kind in Section 5.2. In a term, the $y$ ’s of $s[y/x]$ are exactly the former $x$ ’s, so $(s[y/x])[t/y] = s[t/x]$ ; atomic formulas, $\bot$ and the connectives follow clause by clause. For $\forall x\, \psi$ , both sides are $\forall x\, \psi$ , since substitution for $x$ stops at $\forall x$ and $y$ does not appear in $\psi$ (the second fact of Section 5.2). For $\forall z\, \psi$ with $z$ not $x$ , also $z$ is not $y$ , because $y$ does not appear in $\varphi$ ; so both substitutions pass under the quantifier and the induction hypothesis applies, and $\exists$ is the same. Now let $y$ and $y'$ be two admissible choices. If they are the same variable there is nothing to show. Otherwise $y'$ does not appear in $\varphi[y/x] \to y = x$ , since it is neither $x$ nor $y$ and does not appear in $\varphi$ ; so the bound $y$ of $\forall y\, (\varphi[y/x] \to y = x)$ may be renamed $y'$ , which gives $\forall y'\, \bigl( (\varphi[y/x])[y'/y] \to y' = x \bigr)$ . By the fact with $t = y'$ , this is $\forall y'\, (\varphi[y'/x] \to y' = x)$ , the formula written with $y'$ .

Examples. Simplest first; each is read over the domain named, with the informal truth of Section 5.1.

Over $\mathbb{R}$ , $\exists! x\, (x + 2 = 5)$ is true. Existence: $3 + 2 = 5$ . Uniqueness: if $y + 2 = 5$ , then subtracting $2$ gives $y = 3$ , so $y$ is the $x$ already found.
Over $\mathbb{N}$ , $\exists! x\, (x \cdot x = 4)$ is true. Existence: $2 \cdot 2 = 4$ . Uniqueness: for a natural number $y$ , if $y \le 1$ then $y \cdot y \le 1$ , and if $y \ge 3$ then $y \cdot y \ge 9$ ; so $y \cdot y = 4$ forces $y = 2$ .
Over $\mathbb{R}$ , $\exists! x\, \forall y\, (x + y = y)$ is true: $0$ is the unique additive identity. Existence: $0 + y = y$ for every $y$ . Uniqueness: suppose $z + y = y$ for every $y$ . Apply this to the one instance $y = 0$ (by $\mathrm{\forall E}$ ): $z + 0 = 0$ . Since also $z + 0 = z$ , symmetry and transitivity give $z = 0$ . The whole uniqueness proof is the choice of the instance $y = 0$ .

Nonexample by minimal change. Keep example 2 and change the domain to $\mathbb{Z}$ . Existence still holds, with the same witness $2$ . Uniqueness fails: $y = -2$ also satisfies $y \cdot y = 4$ , and $-2 \ne 2$ . So over $\mathbb{Z}$ , $\exists! x\, (x \cdot x = 4)$ is false, and the failing clause is exactly the second conjunct.

Quick check. Is $\exists! x\, (x < 1)$ true over $\mathbb{N}$ ? Over $\mathbb{Z}$ ?

Solution. Over $\mathbb{N}$ , yes: $0 < 1$ , and every natural number below $1$ is $0$ . Over $\mathbb{Z}$ , no: existence holds, and uniqueness fails, since $0$ and $-1$ are both below $1$ .

Second readingWhy y must not appear, and a degenerate case

Why $y$ must not appear in $\varphi$ . The condition keeps the new quantifier $\forall y$ from capturing anything of $\varphi$ ’s own. Take $\varphi = (x \le y)$ , in which $y$ is free, and read over $\mathbb{N}$ with $y$ naming $0$ . “There is exactly one natural number $x$ with $x \le 0$ ” is true: $x = 0$ . The formula written with the forbidden bound variable $y$ is $\exists x\, \bigl( x \le y \wedge \forall y\, (y \le y \to y = x) \bigr),$ because $(x \le y)[y/x]$ is $y \le y$ . Its second conjunct says that every natural number equals $x$ , which is false. The free $y$ of $\varphi$ , which was to name $0$ , has been captured by $\forall y$ . With an admissible variable, say $z$ , the formula is $\exists x\, \bigl( x \le y \wedge \forall z\, (z \le y \to z = x) \bigr)$ , which is true.

Degenerate. For any constant $c$ , $\exists! x\, (x = c)$ holds in every domain, and it is derivable from no premises (the derivation follows). By contrast, $\exists! x\, (x = x)$ says that the domain has exactly one element, which is false in $\mathbb{N}$ , $\mathbb{Z}$ and $\mathbb{R}$ : existence holds and uniqueness fails.

The derivation of $\exists! x\, (x = c)$ , with the abbreviation written out, shows that $\exists!$ needs no rules of its own:

c = c

\mathrm{{=}I}

y_0

y_0 = c

asm, for

\mathrm{{{\to}}I}

y_0 = c \to y_0 = c

\mathrm{{{\to}}I}

2–2

\forall y\, (y = c \to y = c)

\mathrm{{\forall}I}

2–3

c = c \wedge \forall y\, (y = c \to y = c)

\mathrm{{\wedge}I}

1, 4

\exists x\, (x = c \wedge \forall y\, (y = c \to y = x))

\mathrm{{\exists}I}

Line 3 closes a box whose only line is its assumption: the box shows $y_0 = c \to y_0 = c$ , as $P \to P$ is shown in Chapter 1. Line 6 is $\mathrm{\exists I}$ with the witness $c$ , and it reads line 5 as $\psi[c/x]$ for $\psi = \bigl( x = c \wedge \forall y\, (y = c \to y = x) \bigr)$ , which marks with $x$ the first $c$ and the last one, and keeps the other two. The choice of which occurrences to mark is the one discussed with Definition 5.5.1.

Warning. Uniqueness is not existence. A uniqueness argument (“suppose $y$ also satisfies $\varphi$ ; then $y = x$ ”) proves nothing about whether anything satisfies $\varphi$ . Over $\mathbb{R}$ , every two solutions of $x^2 = -1$ are equal, vacuously, because there are none; yet no real number is “the” square root of $-1$ . Conversely, an existence proof does not give uniqueness: $x^2 = 1$ has the solution $1$ , and “the solution” would be wrong, since $-1$ is another. Before writing “the”, check both halves.

5.8.2. How uniqueness is used and proved

A proof of “exactly one” rarely follows the shape of Definition 5.8.1, which ties the uniqueness clause to the witness just found. It proves two separate statements: there is at least one, and there is at most one. The second is “any two objects with the property are equal”, and it makes no mention of a witness. The next result says that the two shapes say the same thing.

Proposition 5.8.1 (Two Halves of Unique Existence)

Let $\varphi$ be a formula, $x$ a variable, and $y$ a variable other than $x$ that does not appear in $\varphi$ . Then $\exists! x\, \varphi \;\dashv\vdash\; \exists x\, \varphi \wedge \forall x\, \forall y\, \bigl( \varphi \wedge \varphi[y/x] \to x = y \bigr).$

The right-hand side is “existence and at most one”. Its second conjunct is what a mathematician proves under the heading “uniqueness”: take two objects $x$ and $y$ with the property, and show $x = y$ .

Idea. Both directions are searches in the style of Section 3.1 with the quantifier steps. For $\vdash$ , the premise is an $\exists$ , so open its $\mathrm{\exists E}$ box first, with a witness $x_0$ : inside it, $\varphi[x_0/x]$ gives existence at once by $\mathrm{\exists I}$ , and “at most one” is a $\forall\forall$ goal, which opens two flagged boxes $u_0$ , $v_0$ . Two objects $u_0$ , $v_0$ with the property are each equal to the witness $x_0$ , by the uniqueness clause, and so equal to each other: the witness is the “third point” that links them. For $\dashv$ , open the $\mathrm{\exists E}$ box on $\exists x\, \varphi$ with a witness $x_0$ ; the goal inside is $\exists! x\, \varphi$ , whose witness will be $x_0$ again, and the uniqueness clause for $x_0$ comes from “at most one” applied to the pair $x_0$ , $y_0$ .

The two derivations that carry this out are in the fold below.

Second readingThe proof of the two halves

Proof. Choose four distinct variables $x_0$ , $u_0$ , $v_0$ , $y_0$ that do not appear in $\varphi$ , and none of which is $x$ or $y$ . Three facts about substitution are used throughout. First, since $y$ does not appear in $\varphi$ , $(\varphi[y/x])[t/y]$ is $\varphi[t/x]$ for every term $t$ , the fact proved for the well-definedness of Definition 5.8.1. Second, $\varphi[y/x]$ has no free $x$ (every free $x$ became $y$ ), so it is unchanged by a substitution for $x$ . Third, for a term $t$ that does not contain $y$ , $\varphi[t/x]$ contains no $y$ , so it is unchanged by a substitution for $y$ .

$(\vdash)$ The following is a derivation with premise $\exists! x\, \varphi$ , written out.

\exists x\, (\varphi \wedge \forall y\, (\varphi[y/x] \to y = x))

x_0

\varphi[x_0/x] \wedge \forall y\, (\varphi[y/x] \to y = x_0)

asm, for

\mathrm{{\exists}E}

\varphi[x_0/x]

\mathrm{{\wedge}E}

\forall y\, (\varphi[y/x] \to y = x_0)

\mathrm{{\wedge}E}

\exists x\, \varphi

\mathrm{{\exists}I}

u_0

v_0

\varphi[u_0/x] \wedge \varphi[v_0/x]

asm, for

\mathrm{{{\to}}I}

\varphi[u_0/x]

\mathrm{{\wedge}E}

\varphi[v_0/x]

\mathrm{{\wedge}E}

\varphi[u_0/x] \to u_0 = x_0

\mathrm{{\forall}E}

u_0 = x_0

\mathrm{{{\to}}E}

9, 7

\varphi[v_0/x] \to v_0 = x_0

\mathrm{{\forall}E}

v_0 = x_0

\mathrm{{{\to}}E}

11, 8

v_0 = v_0

\mathrm{{=}I}

x_0 = v_0

\mathrm{{=}E}

12, 13

u_0 = v_0

\mathrm{{=}E}

14, 10

\varphi[u_0/x] \wedge \varphi[v_0/x] \to u_0 = v_0

\mathrm{{{\to}}I}

6–15

\forall y\, (\varphi[u_0/x] \wedge \varphi[y/x] \to u_0 = y)

\mathrm{{\forall}I}

6–16

\forall x\, \forall y\, (\varphi \wedge \varphi[y/x] \to x = y)

\mathrm{{\forall}I}

6–17

\exists x\, \varphi \wedge \forall x\, \forall y\, (\varphi \wedge \varphi[y/x] \to x = y)

\mathrm{{\wedge}I}

5, 18

\exists x\, \varphi \wedge \forall x\, \forall y\, (\varphi \wedge \varphi[y/x] \to x = y)

\mathrm{{\exists}E}

1, 2–19

Lines 9 and 11 are $\mathrm{\forall E}$ on line 4 at $u_0$ and at $v_0$ , by the first substitution fact; each term is a variable not bound in $\varphi[y/x] \to y = x_0$ , so it is free for $y$ there. Lines 13 and 14 are the symmetry of Proposition 5.7.1 (a), written out; line 15 is $\mathrm{{=}E}$ with the equation $x_0 = v_0$ and $\psi = (u_0 = z)$ , which turns line 10 into $u_0 = v_0$ . Line 17 is $\mathrm{\forall I}$ with the flag $v_0$ : line 16 is its instance at $v_0$ (by the third and first substitution facts), and $v_0$ appears in no premise, in no assumption still open at line 17 (only line 2 is, and $v_0$ is not in it), and not in line 17. Line 18 is $\mathrm{\forall I}$ with the flag $u_0$ in the same way; its instance at $u_0$ is line 17, by the second substitution fact. Finally, line 20 closes the $\mathrm{\exists E}$ box: its last line 19 does not contain $x_0$ , and $x_0$ is in neither line 1 nor any open assumption.

$(\dashv)$ The following is a derivation with the right-hand side as premise.

\exists x\, \varphi \wedge \forall x\, \forall y\, (\varphi \wedge \varphi[y/x] \to x = y)

\exists x\, \varphi

\mathrm{{\wedge}E}

\forall x\, \forall y\, (\varphi \wedge \varphi[y/x] \to x = y)

\mathrm{{\wedge}E}

x_0

\varphi[x_0/x]

asm, for

\mathrm{{\exists}E}

y_0

\varphi[y_0/x]

asm, for

\mathrm{{{\to}}I}

\forall y\, (\varphi[x_0/x] \wedge \varphi[y/x] \to x_0 = y)

\mathrm{{\forall}E}

\varphi[x_0/x] \wedge \varphi[y_0/x] \to x_0 = y_0

\mathrm{{\forall}E}

\varphi[x_0/x] \wedge \varphi[y_0/x]

\mathrm{{\wedge}I}

4, 5

x_0 = y_0

\mathrm{{{\to}}E}

7, 8

x_0 = x_0

\mathrm{{=}I}

y_0 = x_0

\mathrm{{=}E}

9, 10

\varphi[y_0/x] \to y_0 = x_0

\mathrm{{{\to}}I}

5–11

\forall y\, (\varphi[y/x] \to y = x_0)

\mathrm{{\forall}I}

5–12

\varphi[x_0/x] \wedge \forall y\, (\varphi[y/x] \to y = x_0)

\mathrm{{\wedge}I}

4, 13

\exists x\, (\varphi \wedge \forall y\, (\varphi[y/x] \to y = x))

\mathrm{{\exists}I}

\exists x\, (\varphi \wedge \forall y\, (\varphi[y/x] \to y = x))

\mathrm{{\exists}E}

2, 4–15

Line 6 is $\mathrm{\forall E}$ at $x_0$ on line 3, by the second substitution fact, and line 7 is $\mathrm{\forall E}$ at $y_0$ on line 6, by the third and first. Lines 10 and 11 are symmetry, written out. Line 13 is $\mathrm{\forall I}$ with the flag $y_0$ : line 12 is its instance at $y_0$ , by the first substitution fact; at line 13 the open assumptions are line 4, which does not contain $y_0$ , the premise does not contain it either, and neither does line 13. Line 15 is $\mathrm{\exists I}$ with the witness $x_0$ , which is free for $x$ since it does not appear in $\varphi$ ; line 14 is its instance at $x_0$ , by the second substitution fact. Line 16 closes the $\mathrm{\exists E}$ box: line 15 does not contain $x_0$ , and $x_0$ is in neither line 2 nor the premise, which is the only assumption open outside the box. This proves both directions.

In practice this is how “there is exactly one” is proved: an existence proof, then a separate “suppose $x$ and $y$ both satisfy $\varphi$ ; then $x = y$ ”.

One more instance: “the maximum”. A maximum of a set $A$ of reals is an element $m \in A$ with $a \le m$ for every $a \in A$ . If $m$ and $m'$ are both maxima, then $m' \le m$ (apply the property of $m$ to the element $m' \in A$ ) and $m \le m'$ (apply the property of $m'$ to $m \in A$ ), so $m = m'$ by the order fact that $a \le b$ and $b \le a$ give $a = b$ . That is “at most one”; a set may have no maximum at all, such as $(0, 1)$ , so existence is a separate question. Only when both halves are known may we write “the maximum of $A$ ”.

5.8.3. Counting with equality

“At least one” is $\exists$ , and “at most one” is the second half of Proposition 5.8.1. Beyond one, counting needs the sign $\ne$ .

Definition 5.8.2 (Counting with Equality)

Let $\varphi$ be a formula, $x$ a variable, and $y$ , $z$ two different variables, other than $x$ , that do not appear in $\varphi$ .

“At least two $x$ satisfy $\varphi$ ” abbreviates $\exists x\, \exists y\, (x \ne y \wedge \varphi \wedge \varphi[y/x])$ .
“At most one $x$ satisfies $\varphi$ ” abbreviates $\forall x\, \forall y\, (\varphi \wedge \varphi[y/x] \to x = y)$ .
“At most two $x$ satisfy $\varphi$ ” abbreviates $\forall x\, \forall y\, \forall z\, (\varphi \wedge \varphi[y/x] \wedge \varphi[z/x] \to x = y \vee x = z \vee y = z)$ .
“Exactly two $x$ satisfy $\varphi$ ” abbreviates the conjunction of “at least two” and “at most two”.

For a number $n \ge 2$ , “at least $n$ ” uses $n$ different variables $x_1, \dots, x_n$ that do not appear in $\varphi$ , and asks for all $n(n - 1)/2$ inequalities $x_i \ne x_j$ together with $\varphi$ at each; “at most $n$ ” says that among any $n + 1$ objects satisfying $\varphi$ , two are equal; “exactly $n$ ” is both.

In words: two letters count two objects only when the formula says that they differ, and “at most two” says that three letters satisfying $\varphi$ cannot name three different objects. As with $\exists!$ , these are abbreviations, not new symbols, and $\exists!$ stays the only counting shorthand.

Example (Exactly Two Square Roots of One)

Over $\mathbb{R}$ , show that exactly two $x$ satisfy $x \cdot x = 1$ .

Solution. At least two: the witnesses $1$ and $-1$ : $1 \ne -1$ , $1 \cdot 1 = 1$ and $(-1) \cdot (-1) = 1$ .

At most two: let $u$ , $v$ , $w$ be real numbers with $u \cdot u = v \cdot v = w \cdot w = 1$ . Each is $1$ or $-1$ , since $y \cdot y = 1$ gives $(y - 1)(y + 1) = 0$ . If $u = v$ , the disjunction $u = v \vee u = w \vee v = w$ holds. Otherwise one of $u$ , $v$ is $1$ and the other $-1$ , and $w$ , being $1$ or $-1$ , equals one of them. Three letters, at most two objects: that is what “at most two” means.

Warning. Different letters, perhaps the same object. $\exists x\, \exists y\, (x \cdot x = 1 \wedge y \cdot y = 1)$ is true over $\mathbb{R}$ with $x$ and $y$ both naming $1$ : it says no more than $\exists x\, (x \cdot x = 1)$ . Two letters count two objects only when the formula says $x \ne y$ . The same holds in derivations: two $\mathrm{\exists E}$ boxes with the names $x_0$ and $y_0$ may have named the same object, and nothing gives $x_0 \ne y_0$ .

Quick check. Write “at least two primes are even” with $\mathrm{Prime}$ and $\mathrm{Even}$ , and decide it over $\mathbb{N}$ .

Solution. $\exists x\, \exists y\, \bigl( x \ne y \wedge (\mathrm{Prime}(x) \wedge \mathrm{Even}(x)) \wedge (\mathrm{Prime}(y) \wedge \mathrm{Even}(y)) \bigr)$ . It is false: an even prime is divisible by $2$ , so it is $2$ , and any two even primes are equal.

Only, except and the smallest are counting words too; the drill at the end of the section translates them.

5.8.4. The $x$ such that $\varphi$

Once there is exactly one $x$ with $\varphi$ , mathematics names it: “the maximum of $A$ ”, “the additive inverse of $a$ ”, “ $\sqrt 2$ ”. The name is then used like a constant, because the proof has earned it.

Definition 5.8.3 (Definite Description)

Let $\Gamma$ be a list of formulas and $\varphi$ a formula whose only free variable is $x$ , and suppose $\Gamma \vdash \exists! x\, \varphi$ . Introducing a name for the $x$ such that $\varphi$ means taking a constant $c$ that appears neither in $\Gamma$ nor in $\varphi$ , and letting derivations from $\Gamma$ use the defining line $\varphi[c/x]$ as one more premise. The phrase “the $x$ such that $\varphi$ ” names $c$ .

In words, and why both halves are needed: existence is what makes the defining line safe, and the proposition at the end of this section shows that it proves nothing new about the old symbols. Uniqueness is what makes the word “the” honest. If $c$ and $c'$ are both introduced for $\varphi$ , then $\Gamma, \varphi[c/x], \varphi[c'/x] \vdash c = c'$ : take the “at most one” half of Proposition 5.8.1, instantiate it at $c$ and at $c'$ ( $\mathrm{\forall E}$ twice, with the substitution facts used in the proof of Proposition 5.8.1), and fire it by $\mathrm{\wedge I}$ and $\mathrm{{\to}E}$ . So every proof that names the $x$ such that $\varphi$ names the same object.

Russell’s unpacking. A sentence about the $x$ such that $\varphi$ can be unpacked into one that names nothing. Write $\mathrm{Max}(A, m)$ for “ $m$ is a maximum of $A$ ”, that is, $m \in A \wedge \forall a \in A\; (a \le m)$ (the paragraph “One more instance” above). “The maximum of $A$ is less than $2$ ” unpacks to $\exists m\, \bigl( \mathrm{Max}(A, m) \wedge \forall y\, (\mathrm{Max}(A, y) \to y = m) \wedge m < 2 \bigr):$ there is exactly one maximum, and it is less than $2$ .

Two readings of a negation. When nothing satisfies $\varphi$ , the unpacked sentence is false, and a negation can be read two ways. The interval $A = (0, 1)$ has no maximum: an $m \in A$ is exceeded by $(m + 1)/2$ , which is also in $A$ . Read “the maximum of $A$ is not $1$ ” with the negation inside, $\exists m\, (\mathrm{Max}(A, m) \wedge \forall y\, (\mathrm{Max}(A, y) \to y = m) \wedge m \ne 1)$ : it is false, since there is no $m$ . Read it with the negation outside, $\neg\exists m\, (\mathrm{Max}(A, m) \wedge \forall y\, (\mathrm{Max}(A, y) \to y = m) \wedge m = 1)$ : it is true. The two readings agree whenever there is exactly one maximum, which is why “the” waits for $\exists!$ . The same trap sits in “ $\lim a_n \ne 0$ ” for a sequence with no limit, and analysis writes instead “the sequence converges, and its limit is not $0$ ”.

Quick check. Over $\mathbb{R}$ , may a proof speak of “the $x$ with $x \cdot x = 2$ ”? Of “the $x \ge 0$ with $x \cdot x = 2$ ”?

Solution. The first, no: $\sqrt 2$ and $-\sqrt 2$ both have square $2$ , so uniqueness fails. The second, yes: existence is the school fact of Section 5.1 ( $\sqrt 2$ exists), and uniqueness holds, since two non-negative numbers with the same square are equal (if $0 \le u < v$ , then $u \cdot u < v \cdot v$ ).

5.8.5. A function symbol and its graph

A function symbol gives every object exactly one value, since every term names an object (Section 5.2). A two-place predicate $G(x, y)$ may or may not behave like that. Call $G$ the graph of a function when $\forall x\, \exists! y\, G(x, y)$ : every $x$ has exactly one partner. Then a new function symbol $f$ may be introduced with the defining line $\forall x\, G(x, f(x))$ , and $f(t)$ is “the $y$ such that $G(t, y)$ ”: the name of the last subsection, with $x$ as a parameter.

Over $\mathbb{R}$ , $G(x, y)$ : $y = x \cdot x + 1$ is the graph of a function (existence: $y = x \cdot x + 1$ itself; uniqueness: two numbers equal to $x \cdot x + 1$ are equal). $G(x, y)$ : $y \cdot y = x$ is not: $x = -1$ has no partner, and $x = 4$ has two, $2$ and $-2$ . For $x \ge 0$ , the predicate $y \ge 0 \wedge y \cdot y = x$ gives exactly one partner, and the function it defines is $\sqrt{x}$ , written only under the hypothesis $x \ge 0$ (the fold on partial terms in Section 5.2).

So “a function” and “a relation in which every object has exactly one partner” are two ways of saying the same thing; the function symbol is the shorter.

Quick check. Over $\mathbb{Z}$ , is $x = 2 \cdot y$ the graph of a function, with $y$ as the value at $x$ ? Is $y = 2 \cdot x$ ?

Solution. The first is not: $x = 1$ has no partner, since no integer $y$ has $2y = 1$ . The second is: each $x$ has exactly one partner, $2x$ ; the function is $f(x) = 2x$ .

5.8.6. Definitions add words, not facts

“An integer $n$ is even if $n = 2k$ for some integer $k$ ” adds a predicate symbol with its definition $\forall x\, (\mathrm{Even}(x) \leftrightarrow \exists k\, (x = 2 \cdot k))$ . “We define $\left| x \right|$ to be $x$ if $x \ge 0$ and $-x$ otherwise” adds a function symbol. Its graph $G(x, y)$ : $(x \ge 0 \wedge y = x) \vee (x < 0 \wedge y = -x)$ gives each $x$ exactly one partner (one of $x \ge 0$ , $x < 0$ holds and gives its $y$ , and the two cases exclude each other), and $\left| \cdot \right|$ is introduced by $\forall x\, G(x, \left| x \right|)$ . A definition is a new premise, and premises prove things. The next result says what a definition can prove: nothing new about the old symbols.

Proposition 5.8.2 (Definitions Prove Nothing New)

Let $\Gamma$ be a list of formulas and $\psi$ a formula.

(a) Let $P$ be a one-place predicate symbol that appears neither in $\Gamma$ nor in $\psi$ , and $\varphi$ a formula in which $P$ does not appear and whose only free variable is $x$ . If $\Gamma, \forall x\, (P(x) \leftrightarrow \varphi) \vdash \psi$ , then $\Gamma \vdash \psi$ .
(b) Let $\varphi$ be a formula whose only free variable is $x$ , and $c$ a constant that appears in none of $\Gamma$ , $\varphi$ , $\psi$ . If $\Gamma \vdash \exists x\, \varphi$ and $\Gamma, \varphi[c/x] \vdash \psi$ , then $\Gamma \vdash \psi$ .

In words: whatever is proved with a defined symbol, about symbols that were there before it, could have been proved without it. A definition makes proofs shorter, never stronger.

Part (b) asks only for existence; uniqueness, as the subsection on “the $x$ such that $\varphi$ ” said, is what makes “the” name one object. The same holds for predicates with several places, and for a function symbol $f$ introduced by $\forall x\, G(x, f(x))$ once $\forall x\, \exists! y\, G(x, y)$ is proved; we do not prove those cases, and nothing later depends on them.

Idea. For (b), rename $c$ everywhere into a variable that appears nowhere, and put the whole derivation inside an $\mathrm{\exists E}$ box on $\exists x\, \varphi$ . For (a), replace every atomic formula $P(t)$ by $\varphi[t/x]$ ; the definition becomes $\forall x\, (\varphi \leftrightarrow \varphi)$ , which needs no premise. The fold below carries both out.

Second readingWhy definitions prove nothing new

Proof.

(b) Let $D$ be a derivation of $\psi$ from $\Gamma$ and $\varphi[c/x]$ . Choose a variable $x_0$ that appears nowhere in $D$ , $\Gamma$ , $\varphi$ or $\psi$ (a derivation from $\Gamma$ need not write every member of $\Gamma$ ), and replace $c$ by $x_0$ everywhere in $D$ . Every line stays a correct line: the rules treat constants and variables alike as terms; $x_0$ is not a flag or a witness name of $D$ , since it appears nowhere there; and it is bound nowhere, so every “free for” condition still holds. $\Gamma$ and $\psi$ do not contain $c$ and do not change, and the premise $\varphi[c/x]$ becomes $\varphi[x_0/x]$ , since $c$ is not in $\varphi$ . Now take a derivation of $\exists x\, \varphi$ from $\Gamma$ , open an $\mathrm{\exists E}$ box (Definition 5.6.1) with the name $x_0$ and the assumption $\varphi[x_0/x]$ , copy the changed $D$ inside it, and close the box on $\psi$ : by the choice of $x_0$ , it is not in $\psi$ , not in $\exists x\, \varphi$ , and not in $\Gamma$ , which holds the only premises.
(c) Let $D$ be a derivation of $\psi$ from $\Gamma$ and $\forall x\, (P(x) \leftrightarrow \varphi)$ . Rename the bound variables of $\varphi$ to letters that appear nowhere in $D$ (the convention of Section 5.2), and replace every atomic formula $P(t)$ in $D$ by $\varphi[t/x]$ . Because $x$ is the only free variable of $\varphi$ and its bound letters are new, the replacement commutes with every substitution a rule makes and changes no free variable of any line; so every line stays a correct line, and every side condition still holds. $\Gamma$ and $\psi$ do not contain $P$ and do not change; the definition becomes $\forall x\, (\varphi \leftrightarrow \varphi)$ , which is derived from no premises by a flagged box, with a flag $x_0$ that appears nowhere in $\Gamma$ , $\varphi$ or $D$ , ending in $\varphi[x_0/x] \leftrightarrow \varphi[x_0/x]$ , got by $\mathrm{{\leftrightarrow}I}$ from two one-line boxes. Writing that derivation in front of the changed $D$ derives $\psi$ from $\Gamma$ . (After the renaming the defining premise is $\forall x\, (\varphi' \leftrightarrow \varphi)$ , with $\varphi'$ the renamed $\varphi$ , which the convention of Section 5.2 treats as $\forall x\, (\varphi \leftrightarrow \varphi)$ .)

What a definition sounds like. “We define …” and “call $n$ even if …” introduce a symbol with its defining line; the right-hand side must not mention the new symbol, and a function needs exactly one value for each argument. “Let $L$ be the limit of $(a_n)$ ” introduces a name by a description, and may be written only after it has been proved that there is exactly one such $L$ . Every “the” carries that debt; “a limit” does not.

Remark (Looking ahead). Chapter 8 collects “we define …” and “the …” with the other phrases of written proof.

5.8.7. Exercises

A. Check your understanding

Exercise (A1)

(a) Write $\exists! x\, (x \cdot x = 9)$ without the symbol $\exists!$ , and decide whether it is true over $\mathbb{N}$ and over $\mathbb{Z}$ .
(b) Write “exactly two integers $x$ satisfy $x \cdot x = 9$ ” by Definition 5.8.2, and decide it over $\mathbb{Z}$ .
(c) When may a proof write “the $x$ such that $\varphi$ ”, and what may it then use about that object?
(d) State in words the two parts of Proposition 5.8.2.
(e) Exercise B1 of Section 5.7 showed that any two identities of an operation are equal. Explain how to turn its derivation into the second conjunct of Proposition 5.8.1 for $\varphi = \forall z\, (x \cdot z = z \wedge z \cdot x = z)$ .

Solution. (a) $\exists x\, \bigl( x \cdot x = 9 \wedge \forall y\, (y \cdot y = 9 \to y = x) \bigr)$ . Over $\mathbb{N}$ it is true: $x = 3$ works, and a natural number $y$ with $y \cdot y = 9$ is $3$ , since $y \le 2$ gives $y \cdot y \le 4$ and $y \ge 4$ gives $y \cdot y \ge 16$ . Over $\mathbb{Z}$ it is false: whatever $x$ is proposed, $3$ and $-3$ both satisfy $y \cdot y = 9$ , and they cannot both equal $x$ .

(b) $\exists x\, \exists y\, (x \ne y \wedge x \cdot x = 9 \wedge y \cdot y = 9) \wedge \forall x\, \forall y\, \forall z\, (x \cdot x = 9 \wedge y \cdot y = 9 \wedge z \cdot z = 9 \to x = y \vee x = z \vee y = z)$ . True: $3 \ne -3$ are two solutions, and every solution is $3$ or $-3$ (since $(y - 3)(y + 3) = 0$ ), so among three solutions two are equal.

(c) After $\exists! x\, \varphi$ has been proved from the premises in hand. It may use the defining line $\varphi[c/x]$ , and only what follows from it with the premises.

(d) Part (a): adding a predicate symbol by a definition $\forall x\, (P(x) \leftrightarrow \varphi)$ proves nothing new that does not mention $P$ . Part (b): naming a witness of a proved existential by a new constant proves nothing new that does not mention the constant.

(e) Take $\varphi = \forall z\, (x \cdot z = z \wedge z \cdot x = z)$ , and run lines 3–7 again with variables $u_0$ , $v_0$ in place of $e$ , $e'$ : inside flagged boxes for $u_0$ and $v_0$ and a $\mathrm{{\to}I}$ box on $\varphi[u_0/x] \wedge \varphi[v_0/x]$ , the two premises (with $z$ as their bound variable) come from that assumption by $\mathrm{\wedge E}$ , and the same steps give $u_0 = v_0$ . Then $\mathrm{{\to}I}$ and $\mathrm{\forall I}$ twice give $\forall x\, \forall y\, (\varphi \wedge \varphi[y/x] \to x = y)$ , the second conjunct of the proposition. With the existence of one identity as well, Proposition 5.8.1 gives “there is exactly one”.

Exercise (A2: Drill)

Each part takes a line or two. The parts run from writing counting statements, through judging them and the counting words, to descriptions and graphs.

(a) Write $\exists! x\, (x + 1 = 3)$ without $\exists!$ .
(b) Write “at least two elements of $A$ are negative”.
(c) Write “at most two $x$ satisfy $P(x)$ ”.
(d) Write “exactly two $x$ satisfy $P(x)$ ” as one formula of the shape $\exists x\, \exists y\, (\dots \wedge \forall z\, (\dots))$ .
(e) Does $\exists x\, \exists y\, (P(x) \wedge P(y))$ say “at least two $x$ satisfy $P(x)$ ”?
(f) Over $\mathbb{N}$ , translate “ $0$ is the only natural number $n$ with $n + n = n$ ”, and decide it.
(g) Translate “every prime except $2$ is odd”. Does your formula say that $2$ is not odd?
(h) Write “ $m$ is the smallest element of $A$ ”, and say what must be proved before writing “the smallest element of $A$ ”.
(i) In $A = \{2, 3, 4\}$ , ordered by divisibility, which elements are maximal (no other element of $A$ is a multiple of them), and is there a maximum (an element that is a multiple of every element of $A$ )?
(j) $A = (0, 1]$ has no smallest element. Read “the smallest element of $A$ is not positive” both ways, and decide each.
(k) Over $\mathbb{R}$ , does $x \cdot y = 1$ give each $x$ exactly one partner $y$ ? Over the non-zero reals?
(l) A proof says “let $c$ be the real number with $c + 3 = 5$ ”. What must have been proved, and what may be used about $c$ ?

Solution.

(a) $\exists x\, (x + 1 = 3 \wedge \forall y\, (y + 1 = 3 \to y = x))$ .
(b) $\exists x\, \exists y\, (x \ne y \wedge (x \in A \wedge x < 0) \wedge (y \in A \wedge y < 0))$ .
(c) $\forall x\, \forall y\, \forall z\, (P(x) \wedge P(y) \wedge P(z) \to x = y \vee x = z \vee y = z)$ .
(d) $\exists x\, \exists y\, (x \ne y \wedge P(x) \wedge P(y) \wedge \forall z\, (P(z) \to z = x \vee z = y))$ .
(e) No: $x$ and $y$ may name the same object; it says only $\exists x\, P(x)$ .
(f) $0 + 0 = 0 \wedge \forall x\, (x + x = x \to x = 0)$ . True: $x + x = x$ gives $x = 0$ by cancelling $x$ .
(g) $\forall x\, (\mathrm{Prime}(x) \wedge x \ne 2 \to \mathrm{Odd}(x))$ . It says nothing about $2$ . If “except” is meant to say that $2$ is not odd as well, add $\wedge \neg\mathrm{Odd}(2)$ .
(h) $m \in A \wedge \forall a \in A\; (m \le a)$ . Existence only: two smallest elements are each $\le$ the other, hence equal, so uniqueness is automatic.
(i) $3$ and $4$ are maximal; $2$ is not, since $4$ is a multiple of $2$ . There is no maximum: $3$ is not a multiple of $2$ or of $4$ , and $4$ is not a multiple of $3$ ; and $2$ is not a multiple of $3$ either. Maximal and maximum differ.
(j) With $\mathrm{Min}(A, m)$ the formula of (h): negation inside, $\exists m\, (\mathrm{Min}(A, m) \wedge \forall y\, (\mathrm{Min}(A, y) \to y = m) \wedge \neg(m > 0))$ , false, since there is no $m$ . Negation outside, $\neg\exists m\, (\mathrm{Min}(A, m) \wedge \forall y\, (\mathrm{Min}(A, y) \to y = m) \wedge m > 0)$ , true. (For $m \in A$ , $m/2 \in A$ is smaller.)
(k) No: $x = 0$ has none, since $0 \cdot y = 0$ . Over $x \ne 0$ , yes: the partner is $1/x$ , and $x \cdot y = x \cdot y' = 1$ gives $y = y'$ .
(l) $\exists! x\, (x + 3 = 5)$ : existence makes the name safe, uniqueness makes “the” right. It may use the defining line $c + 3 = 5$ , and what follows from it, such as $c = 2$ .

B. Practice

Exercise (B1: Exactly two, by halves)

Over $\mathbb{N}$ , show that exactly two natural numbers $x$ satisfy $x \cdot x < 3$ : write the statement by Definition 5.8.2, then prove “at least two” and “at most two” separately.

Solution. The statement is $\exists x\, \exists y\, (x \ne y \wedge x \cdot x < 3 \wedge y \cdot y < 3) \wedge \forall x\, \forall y\, \forall z\, (x \cdot x < 3 \wedge y \cdot y < 3 \wedge z \cdot z < 3 \to x = y \vee x = z \vee y = z).$

At least two: $0$ and $1$ : $0 \ne 1$ , $0 \cdot 0 = 0 < 3$ and $1 \cdot 1 = 1 < 3$ .

At most two: if $x \cdot x < 3$ then $x \le 1$ , since $x \ge 2$ gives $x \cdot x \ge 4$ ; so $x \in \{0, 1\}$ . Three natural numbers $u$ , $v$ , $w$ with squares below $3$ take values in $\{0, 1\}$ , so two of them are equal. Worked example type: Example (Exactly Two Square Roots of One).

Marking scheme. (10 points) 3: the formula, with $x \ne y$ and the three-way disjunction. 3: “at least two”, with both witnesses and their difference. 4: “at most two”, with $x \le 1$ justified and the pigeonhole step stated. Fatal error (0 for the half): “at least two” written without $x \ne y$ .

Exercise (B2: A unique square root of zero)

Over $\mathbb{R}$ , write $\exists! x\, (x \cdot x = 0)$ without $\exists!$ , and prove it: existence, then uniqueness in the form “suppose $y$ also satisfies …”.

Hint: a product of two non-zero reals is non-zero.

Solution. Written out, the statement is $\exists x\, \bigl( x \cdot x = 0 \wedge \forall y\, (y \cdot y = 0 \to y = x) \bigr)$ . We take the witness $x = 0$ and prove the two conjuncts.

Existence. $0 \cdot 0 = 0$ .

Uniqueness. Let $y$ be a real number, and suppose $y \cdot y = 0$ . If $y \ne 0$ , then $y \cdot y$ is a product of two non-zero reals and so is non-zero, which contradicts $y \cdot y = 0$ . Hence $y = 0$ , which is the witness. Since $y$ was arbitrary, every $y$ with $y \cdot y = 0$ equals $0$ .

So $0$ witnesses the existential, and $\exists! x\, (x \cdot x = 0)$ holds. The rules behind the words: “we take the witness $x = 0$ ” is $\mathrm{\exists I}$ , postponed to the end as usual; “let $y$ be a real number” is a flagged box for $\mathrm{\forall I}$ ; “suppose $y \cdot y = 0$ ” is a $\mathrm{{\to}I}$ box; “if $y \ne 0$ … contradicts” is an $\mathrm{RAA}$ box on $y \ne 0$ . (That box gives $y = 0$ directly; $\mathrm{\neg I}$ would give only $\neg(y \ne 0)$ . Since for reals $y = 0$ or $y \ne 0$ is also a school fact, a proof by cases would do as well.)

Exercise (B3: Exactly one fixed point)

A fixed point of a function $f \colon \mathbb{R} \to \mathbb{R}$ is a real $x$ with $f(x) = x$ .

(a) Formalize “ $f$ has exactly one fixed point” over $\mathbb{R}$ , first with $\exists!$ and then without it.
(b) Write a formula without $\exists!$ that says “ $f$ does not have exactly one fixed point”, in the form “there is none, or there are two different ones”.
(c) Decide the statement of (a) for $f(x) = x \cdot x$ , for $f(x) = x + 1$ and for $f(x) = 2 \cdot x$ , and check your answer against the formula of (b).

Solution. (a) With $\exists!$ : $\exists! x\, (f(x) = x)$ . Written out, with $y$ as the new variable: $\exists x\, \bigl( f(x) = x \wedge \forall y\, (f(y) = y \to y = x) \bigr)$ .

(b) $\neg\exists x\, (f(x) = x) \vee \exists x\, \exists y\, \bigl( f(x) = x \wedge f(y) = y \wedge x \ne y \bigr)$ . Read informally over $\mathbb{R}$ : either no real number is fixed, or two different ones are. That is exactly the failure of “exactly one”. If no $x$ is fixed, the first disjunct holds. If some $x$ is fixed but the uniqueness clause fails for it, then some $y$ is fixed and differs from $x$ . Conversely, either disjunct rules out a unique fixed point: with none there is no witness, and two different fixed points $x \ne y$ would both have to equal any proposed witness $w$ , giving $x = y$ . (Section 6.2 derives such negations mechanically, one quantifier at a time.)

(c) For $f(x) = x \cdot x$ : $x \cdot x = x$ holds for $x = 0$ and for $x = 1$ , so there are two different fixed points; (a) is false, and the second disjunct of (b) is true with $x = 0$ , $y = 1$ . For $f(x) = x + 1$ : $x + 1 = x$ has no solution, so (a) is false and the first disjunct of (b) is true. For $f(x) = 2 \cdot x$ : $2x = x$ gives $x = 0$ , and $0$ is fixed; so (a) is true with the witness $0$ , and both disjuncts of (b) are false.

Exercise (B4: The empty set is unique)

Read the domain as consisting of sets, and let $E$ be the axiom of extensionality, $\forall x\, \forall y\, (\forall z\, (z \in x \leftrightarrow z \in y) \to x = y)$ .

(a) Derive $E, \ \forall z\, \neg(z \in a), \ \forall z\, \neg(z \in b) \vdash a = b$ .
(b) Which half of “there is exactly one set with no elements” does (a) prove, and what would give the other half?
(c) Suppose also $\exists x\, \forall z\, \neg(z \in x)$ . Which result of this section gives $\exists! x\, \forall z\, \neg(z \in x)$ , and what may a proof then write?

Solution.

(a) The goal $a = b$ is the consequent of an instance of $E$ ; its hypothesis $\forall z\, (z \in a \leftrightarrow z \in b)$ is built in a flagged box, each direction of the biconditional by $\mathrm{\bot E}$ .
1 $\forall x\, \forall y\, (\forall z\, (z \in x \leftrightarrow z \in y) \to x = y)$
2 $\forall z\, \neg (z \in a)$
3 $\forall z\, \neg (z \in b)$
4 $z_0$ $z_0 \in a$ asm, for $\mathrm{{{\leftrightarrow}}I}$
5 $\neg (z_0 \in a)$ $\mathrm{{\forall}E}$ 2
6 $\bot$ $\mathrm{{\neg}E}$ 4, 5
7 $z_0 \in b$ $\mathrm{{\bot}E}$ 6
8 $z_0 \in b$ asm, for $\mathrm{{{\leftrightarrow}}I}$
9 $\neg (z_0 \in b)$ $\mathrm{{\forall}E}$ 3
10 $\bot$ $\mathrm{{\neg}E}$ 8, 9
11 $z_0 \in a$ $\mathrm{{\bot}E}$ 10
12 $z_0 \in a \leftrightarrow z_0 \in b$ $\mathrm{{{\leftrightarrow}}I}$ 4–7, 8–11
13 $\forall z\, (z \in a \leftrightarrow z \in b)$ $\mathrm{{\forall}I}$ 4–12
14 $\forall y\, (\forall z\, (z \in a \leftrightarrow z \in y) \to a = y)$ $\mathrm{{\forall}E}$ 1
15 $\forall z\, (z \in a \leftrightarrow z \in b) \to a = b$ $\mathrm{{\forall}E}$ 14
16 $a = b$ $\mathrm{{{\to}}E}$ 15, 13
(b) “At most one”: any two sets without elements are equal. The other half, “at least one”, needs a premise of its own, an axiom saying that a set without elements exists: from $E$ alone the claim $\exists x\, \forall z\, \neg(z \in x)$ breaks. Counter-reading: the domain $\{0\}$ , with $0 \in 0$ . $E$ is true, since there is only one object and so $x = y$ holds for every $x$ , $y$ ; and $\exists x\, \forall z\, \neg(z \in x)$ is false, since the only object, $0$ , has the element $0$ .
(c) Run (a) with flags $x_0$ , $y_0$ in place of $a$ , $b$ , inside a $\mathrm{{\to}I}$ box on $\forall z\, \neg(z \in x_0) \wedge \forall z\, \neg(z \in y_0)$ ( $\mathrm{\wedge E}$ gives the two premises), and close with $\mathrm{{\to}I}$ and $\mathrm{\forall I}$ twice: that is the second conjunct of Proposition 5.8.1 for $\varphi = \forall z\, \neg(z \in x)$ . With the existence premise, the direction $\dashv$ of Proposition 5.8.1 gives $\exists! x\, \forall z\, \neg(z \in x)$ , and by Definition 5.8.3 a proof may now say “the empty set” and name it $\emptyset$ . Worked example types: Example (Equal Sets Have the Same Elements) (Section 5.7); the two halves of Proposition 5.8.1.

Marking scheme. (10 points) 4: (a), the biconditional built by $\mathrm{{\leftrightarrow}I}$ from two boxes, each closed by $\mathrm{\bot E}$ , then $\mathrm{\forall I}$ , two $\mathrm{\forall E}$ on $E$ and $\mathrm{{\to}E}$ . 3: (b), “at most one” (1), existence as a separate premise (1), and the counter-reading with $E$ checked true and the existence claim false (1). 3: (c), the flags and the $\mathrm{{\to}I}$ box, the right direction of Proposition 5.8.1, and the license to write “the”. Fatal error (0 for (a)): $a = b$ “by extensionality” with no instance of $E$ written.

Exercise (B5: Composites of one-to-one maps)

A function symbol $f$ is one-to-one if $\forall x\, \forall y\, (f(x) = f(y) \to x = y)$ . Derive $\forall x\, \forall y\, (f(x) = f(y) \to x = y), \;\; \forall x\, \forall y\, (g(x) = g(y) \to x = y) \;\vdash\; \forall x\, \forall y\, (f(g(x)) = f(g(y)) \to x = y),$ then write the proof in two sentences.

Solution.

\forall x\, \forall y\, (f(x) = f(y) \to x = y)

\forall x\, \forall y\, (g(x) = g(y) \to x = y)

x_0

y_0

f(g(x_0)) = f(g(y_0))

asm, for

\mathrm{{{\to}}I}

\forall y\, (f(g(x_0)) = f(y) \to g(x_0) = y)

\mathrm{{\forall}E}

f(g(x_0)) = f(g(y_0)) \to g(x_0) = g(y_0)

\mathrm{{\forall}E}

g(x_0) = g(y_0)

\mathrm{{{\to}}E}

5, 3

\forall y\, (g(x_0) = g(y) \to x_0 = y)

\mathrm{{\forall}E}

g(x_0) = g(y_0) \to x_0 = y_0

\mathrm{{\forall}E}

x_0 = y_0

\mathrm{{{\to}}E}

8, 6

f(g(x_0)) = f(g(y_0)) \to x_0 = y_0

\mathrm{{{\to}}I}

3–9

\forall y\, (f(g(x_0)) = f(g(y)) \to x_0 = y)

\mathrm{{\forall}I}

3–10

\forall x\, \forall y\, (f(g(x)) = f(g(y)) \to x = y)

\mathrm{{\forall}I}

3–11

Lines 4 and 5 instantiate the premise for $f$ at the compound terms $g(x_0)$ and $g(y_0)$ : the move instantiate at the term you need. In prose: “Let $x$ and $y$ satisfy $f(g(x)) = f(g(y))$ . Since $f$ is one-to-one, $g(x) = g(y)$ , and since $g$ is one-to-one, $x = y$ .”

Marking scheme. (10 points) 2: the two flags and the $\mathrm{{\to}I}$ box. 4: the $\mathrm{\forall E}$ steps at $g(x_0)$ , $g(y_0)$ , then at $x_0$ , $y_0$ , each with $\mathrm{{\to}E}$ . 2: the closing $\mathrm{\forall I}$ lines with the flag checks. 2: the prose, one sentence per use of one-to-one. Fatal error (0 for the derivation): the premise for $f$ instantiated at $x_0$ , $y_0$ .

C. Going deeper

Exercise (C1: Two unique quantifiers do not commute)

Show that $\exists! x\, \exists! y\, R(x, y)$ and $\exists! y\, \exists! x\, R(x, y)$ can have different truth values, by giving a finite domain $D$ and a two-place relation $R$ on it for which the first is true and the second false. Check both, reading $\exists!$ informally.

Hint: first say in words what each sentence claims about the rows and columns of a table of $R$ .

Solution. What any answer must satisfy. Call $x$ single if exactly one $y$ has $R(x, y)$ , and call $y$ co-single if exactly one $x$ has $R(x, y)$ . The first sentence says that exactly one element is single. The second says that exactly one element is co-single. So an answer needs exactly one single element and a number of co-single elements other than one: none, or two or more.

An example. Take $D = \{0, 1, 2\}$ and $R = \{(1, 2), (2, 0), (2, 1)\}$ .

Single elements: $0$ has no partner, $1$ has exactly one ( $2$ ), and $2$ has two ( $0$ and $1$ ). So $1$ is the only single element, and $\exists! x\, \exists! y\, R(x, y)$ is true, with the witness $1$ .
Co-single elements: $y = 0$ is reached only from $x = 2$ ; $y = 1$ only from $x = 2$ ; $y = 2$ only from $x = 1$ . All three are co-single, so there is not exactly one, and $\exists! y\, \exists! x\, R(x, y)$ is false.

No example exists on one or two elements (there are only $2 + 16 = 18$ relations on such domains). On one element, $0$ is single and co-single exactly when $R(0, 0)$ holds, so the two sentences agree. On two elements, suppose exactly one element is single; after relabeling, call it $0$ , and let $c$ be its only partner. Then $1$ is not single, so it has no partners or two. If it has none, column $c$ has one entry and the other column has none. If it has two, column $c$ has two entries and the other column has one. Either way exactly one element is co-single. Exchanging the roles of rows and columns gives the converse, so the two sentences have the same truth value. Three elements is therefore the smallest possible domain.

The moral: $\exists!$ is not a quantifier that commutes with its own kind, as two $\exists$ ’s do. “Exactly one” hides a $\forall$ (the uniqueness clause), and the order of a $\forall$ and an $\exists$ matters.

Exercise (C2: “At most one”, two ways)

Let $P$ be a one-place predicate symbol. Derive both directions of $\forall x\, \forall y\, \bigl( P(x) \wedge P(y) \to x = y \bigr) \;\dashv\vdash\; \neg\exists x\, \exists y\, \bigl( (P(x) \wedge P(y)) \wedge x \ne y \bigr),$ and say which of your two derivations uses $\mathrm{RAA}$ , and at which line.

Solution (Hint 1). The right-hand side is a negation: for $\vdash$ , open a $\mathrm{\neg I}$ box, and inside it two $\mathrm{\exists E}$ boxes. For $\dashv$ , the goal is $\forall\forall$ , then an implication, then an equation.

Solution (Hint 2). In the $\dashv$ direction, open flagged boxes for $x_0$ and $y_0$ and a $\mathrm{{\to}I}$ box on $P(x_0) \wedge P(y_0)$ . The goal is now the atomic formula $x_0 = y_0$ . Which resources can give it?

Solution. $(\vdash)$ The goal is a negation, so a $\mathrm{\neg I}$ box opens on $\exists x\, \exists y\, (\dots)$ ; inside, the premise-directed step opens an $\mathrm{\exists E}$ box for each $\exists$ , with the goal $\bot$ as each box’s last line. The premise, instantiated at the two witnesses, gives $x_0 = y_0$ , which clashes with $x_0 \ne y_0$ .

\forall x\, \forall y\, (P(x) \wedge P(y) \to x = y)

\exists x\, \exists y\, ((P(x) \wedge P(y)) \wedge x \neq y)

asm, for

\mathrm{{\neg}I}

x_0

\exists y\, ((P(x_0) \wedge P(y)) \wedge x_0 \neq y)

asm, for

\mathrm{{\exists}E}

y_0

(P(x_0) \wedge P(y_0)) \wedge x_0 \neq y_0

asm, for

\mathrm{{\exists}E}

P(x_0) \wedge P(y_0)

\mathrm{{\wedge}E}

x_0 \neq y_0

\mathrm{{\wedge}E}

\forall y\, (P(x_0) \wedge P(y) \to x_0 = y)

\mathrm{{\forall}E}

P(x_0) \wedge P(y_0) \to x_0 = y_0

\mathrm{{\forall}E}

x_0 = y_0

\mathrm{{{\to}}E}

8, 5

\bot

\mathrm{{\neg}E}

9, 6

\bot

\mathrm{{\exists}E}

3, 4–10

\bot

\mathrm{{\exists}E}

2, 3–11

\neg \exists x\, \exists y\, ((P(x) \wedge P(y)) \wedge x \neq y)

\mathrm{{\neg}I}

2–12

The brackets in the statement are written out because the default groups a longer conjunction to the right (Section 4.5); with the grouping $(P(x_0) \wedge P(y_0)) \wedge x_0 \ne y_0$ on line 4, $\mathrm{\wedge E}$ takes out its two halves on lines 5 and 6. At line 11, $y_0$ is not in $\bot$ , not in line 3, not in the premise, and not in the assumptions still open (lines 2 and 3). At line 12 the same holds for $x_0$ , with line 2 the only open assumption.

$(\dashv)$ The goal-directed steps open flagged boxes for $x_0$ and $y_0$ and a $\mathrm{{\to}I}$ box on $P(x_0) \wedge P(y_0)$ , leaving the goal $x_0 = y_0$ . No resource gives an equation, so the search is stuck, and step 5 of the method applies: an $\mathrm{RAA}$ box on $x_0 \ne y_0$ . Inside, $\mathrm{\wedge I}$ and two $\mathrm{\exists I}$ steps rebuild the formula that the premise denies.

\neg \exists x\, \exists y\, ((P(x) \wedge P(y)) \wedge x \neq y)

x_0

y_0

P(x_0) \wedge P(y_0)

asm, for

\mathrm{{{\to}}I}

x_0 \neq y_0

asm, for

\mathrm{RAA}

(P(x_0) \wedge P(y_0)) \wedge x_0 \neq y_0

\mathrm{{\wedge}I}

2, 3

\exists y\, ((P(x_0) \wedge P(y)) \wedge x_0 \neq y)

\mathrm{{\exists}I}

\exists x\, \exists y\, ((P(x) \wedge P(y)) \wedge x \neq y)

\mathrm{{\exists}I}

\bot

\mathrm{{\neg}E}

6, 1

x_0 = y_0

\mathrm{RAA}

3–7

P(x_0) \wedge P(y_0) \to x_0 = y_0

\mathrm{{{\to}}I}

2–8

\forall y\, (P(x_0) \wedge P(y) \to x_0 = y)

\mathrm{{\forall}I}

2–9

\forall x\, \forall y\, (P(x) \wedge P(y) \to x = y)

\mathrm{{\forall}I}

2–10

The $\dashv$ derivation uses $\mathrm{RAA}$ , at line 8: the box opens with $x_0 \ne y_0$ , that is $\neg(x_0 = y_0)$ , and closes with $x_0 = y_0$ . Closing it by $\mathrm{\neg I}$ instead would give $\neg\neg(x_0 = y_0)$ , and no rule of Chapter 1 or Sections 2.1–2.4 removes the double negation. (With the derived rule $\mathrm{\neg\neg E}$ of Section 2.5, that $\mathrm{\neg I}$ box followed by $\mathrm{\neg\neg E}$ is an equally good derivation; its classical step is the $\mathrm{\neg\neg E}$ line, which hides an $\mathrm{RAA}$ .) The $\vdash$ derivation uses no classical rule.

Marking scheme. (10 points) - 2: $\vdash$ : opens a $\mathrm{\neg I}$ box on the existential, with the goal $\bot$ . - 2: $\vdash$ : two $\mathrm{\exists E}$ boxes with fresh witnesses, each ending in $\bot$ , and the premise instantiated at those witnesses. - 2: $\dashv$ : two flagged boxes and a $\mathrm{{\to}I}$ box, in the order read off the goal. - 2: $\dashv$ : an $\mathrm{RAA}$ box on $x_0 \ne y_0$ , with the clash obtained by $\mathrm{\wedge I}$ and two $\mathrm{\exists I}$ steps. - 2: names the $\dashv$ direction as the one using $\mathrm{RAA}$ , and the line. - A $\mathrm{\neg I}$ box on $x_0 \ne y_0$ followed by $\mathrm{\neg\neg E}$ , or an $\mathrm{LEM}$ split on $x_0 = y_0$ whose second case reaches $\bot$ the same way (then $\mathrm{\bot E}$ ), earns the 2 points of the $\mathrm{RAA}$ -box line; for the naming line, the reader names the $\mathrm{\neg\neg E}$ or $\mathrm{LEM}$ line as the classical step, a derived rule whose derivation uses $\mathrm{RAA}$ (Section 2.5). Fatal errors (0 for the step): an $\mathrm{\exists E}$ box closing on a line that contains its witness; a $\mathrm{\forall I}$ over a name in an open assumption; $\mathrm{\neg I}$ claimed to give $x_0 = y_0$ .

Exercise (C3: One and one make two)

Let $P$ and $Q$ be one-place predicate symbols. Show that from $\exists! x\, P(x)$ , $\exists! x\, Q(x)$ and $\neg\exists x\, (P(x) \wedge Q(x))$ it follows that exactly two $x$ satisfy $P(x) \vee Q(x)$ , in the form $\exists x\, \exists y\, \bigl( x \ne y \wedge (P(x) \vee Q(x)) \wedge (P(y) \vee Q(y)) \wedge \forall z\, (P(z) \vee Q(z) \to z = x \vee z = y) \bigr).$ Give the proof in numbered steps, naming the rule behind each; a full derivation is not required. Which premise does the conjunct $x \ne y$ need, and what happens without it?

Solution.

By Proposition 5.8.1, the first premise gives $\exists x\, P(x)$ and “at most one $P$ ”, and the second gives $\exists x\, Q(x)$ and “at most one $Q$ ” ( $\mathrm{\wedge E}$ ).
Open two $\mathrm{\exists E}$ boxes early, with different names: $P(a_0)$ and $Q(b_0)$ , both aimed at the goal.
$a_0 \ne b_0$ : in a $\mathrm{\neg I}$ box on $a_0 = b_0$ , $\mathrm{{=}E}$ turns $P(a_0)$ into $P(b_0)$ ; $\mathrm{\wedge I}$ with $Q(b_0)$ and $\mathrm{\exists I}$ give $\exists x\, (P(x) \wedge Q(x))$ , which $\mathrm{\neg E}$ clashes with the third premise.
$P(a_0) \vee Q(a_0)$ and $P(b_0) \vee Q(b_0)$ by $\mathrm{\vee I}$ .
Let $z_0$ be arbitrary (a flagged box) with $P(z_0) \vee Q(z_0)$ (a $\mathrm{{\to}I}$ box), and split by $\mathrm{\vee E}$ . If $P(z_0)$ : “at most one $P$ ” at $z_0$ and $a_0$ ( $\mathrm{\forall E}$ twice, $\mathrm{\wedge I}$ , $\mathrm{{\to}E}$ ) gives $z_0 = a_0$ , and $\mathrm{\vee I}$ gives $z_0 = a_0 \vee z_0 = b_0$ . If $Q(z_0)$ : “at most one $Q$ ” at $z_0$ and $b_0$ gives $z_0 = b_0$ , and $\mathrm{\vee I}$ again.
$\mathrm{{\to}I}$ and $\mathrm{\forall I}$ give the last conjunct; $\mathrm{\wedge I}$ joins the four; $\mathrm{\exists I}$ with the witness $b_0$ for $y$ , then $a_0$ for $x$ . Both $\mathrm{\exists E}$ boxes close, since the goal mentions neither name.

The third premise is used only in step 3. Without it the conclusion breaks: the domain $\{0\}$ with $P$ and $Q$ both true of $0$ makes the first two premises true, and only one object satisfies $P(x) \vee Q(x)$ .

Marking scheme. (10 points) 2: the two halves of each premise by Proposition 5.8.1. 1: two $\mathrm{\exists E}$ boxes with different names. 2: $a_0 \ne b_0$ by $\mathrm{\neg I}$ , $\mathrm{{=}E}$ and the third premise. 3: the last conjunct by the flagged box, the $\mathrm{{\to}I}$ box and $\mathrm{\vee E}$ , each case using the right “at most one”. 1: the closing $\mathrm{\exists I}$ order and the box conditions. 1: the counter-reading without the third premise. Fatal errors (0 for the step): $a_0 \ne b_0$ asserted because the names differ (the warning “Different letters, perhaps the same object”); an $\mathrm{\exists E}$ box closed on a line that mentions $a_0$ or $b_0$ .

R. Review

Exercise (R1)

Consider the terms built from variables, the constant $0$ and the two-place function symbol $+$ . Show that in every such term the number of occurrences of $+$ is one less than the number of occurrences of variables and constants, counted together. Check it on $(x + 0) + (y + x)$ .

Solution. For a term $t$ , let $a(t)$ count the occurrences of variables and constants in $t$ , and $p(t)$ those of $+$ . We show $p(t) = a(t) - 1$ for every $t$ , by induction on the clauses of Definition 5.2.1, the method of Theorem 4.3.1 (Section 4.3).

Base: $t$ is a variable or $0$ . Then $p(t) = 0$ and $a(t) = 1$ .

Step: $t$ is $t_1 + t_2$ , and the claim holds for $t_1$ and $t_2$ . Then $p(t) = p(t_1) + p(t_2) + 1 = (a(t_1) - 1) + (a(t_2) - 1) + 1 = a(t_1) + a(t_2) - 1 = a(t) - 1.$

The term $(x + 0) + (y + x)$ has four occurrences of variables and constants and three of $+$ . This is the counting argument of Lemma 4.3.2 (Section 4.3), on new data. About 10 minutes.

Marking scheme. (10 points) 2: $a$ and $p$ defined. 3: the base case, both kinds of atomic term. 4: the step, with the hypothesis used for both $t_1$ and $t_2$ and the $+1$ for the new symbol. 1: the check. Fatal error (0 for the step): induction on the length of the term with no case for $t_1 + t_2$ .

Exercise (R2)

Derive $\forall x\, (\neg Q(x) \to \neg P(x)) \vdash \forall x\, (P(x) \to Q(x))$ , and name the line that uses a classical rule.

Solution.

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

x_0

P(x_0)

asm, for

\mathrm{{{\to}}I}

\neg Q(x_0) \to \neg P(x_0)

\mathrm{{\forall}E}

\neg Q(x_0)

asm, for

\mathrm{RAA}

\neg P(x_0)

\mathrm{{{\to}}E}

3, 4

\bot

\mathrm{{\neg}E}

2, 5

Q(x_0)

\mathrm{RAA}

4–6

P(x_0) \to Q(x_0)

\mathrm{{{\to}}I}

2–7

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

\mathrm{{\forall}I}

2–8

Line 9 cites the flagged box from line 2, the convention for a flagged box that immediately contains another; $x_0$ is in no premise, in no open assumption, and not in line 9. Lines 2 and 4–8 are the derivation of Proposition 2.5.2 (Section 2.5) at $P(x_0)$ , $Q(x_0)$ , with line 3 as its premise. The classical line is line 7, $\mathrm{RAA}$ (Definition 2.5.1). About 10 minutes.

Marking scheme. (10 points) 2: the flagged box opened first and closed by $\mathrm{\forall I}$ with the flag checked. 2: $\mathrm{\forall E}$ at the flag. 4: the $\mathrm{{\to}I}$ box and, inside it, the $\mathrm{RAA}$ box on $\neg Q(x_0)$ . 2: line 7 named as the classical line. A $\mathrm{\neg I}$ box on $\neg Q(x_0)$ followed by $\mathrm{\neg\neg E}$ , or Proposition 2.5.2 used as a derived rule on line 3, earns the 4 points of the box line; its classical line (the $\mathrm{\neg\neg E}$ line, or the derived-rule line, whose derivation uses $\mathrm{RAA}$ ) earns the naming 2. Fatal error (0): $\mathrm{\forall E}$ outside the flagged box at a constant, then $\mathrm{\forall I}$ over that constant.

Exercise (R3)

You have derived $(P \wedge Q) \to R \vdash P \to (Q \to R)$ . Derive $\forall x\, ((P(x) \wedge Q(x)) \to R(x)) \vdash \forall x\, (P(x) \to (Q(x) \to R(x)))$ , and say which lines are the propositional derivation and what the quantifier adds.

Solution.

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

x_0

(P(x_0) \wedge Q(x_0)) \to R(x_0)

\mathrm{{\forall}E}

P(x_0)

asm, for

\mathrm{{{\to}}I}

Q(x_0)

asm, for

\mathrm{{{\to}}I}

P(x_0) \wedge Q(x_0)

\mathrm{{\wedge}I}

3, 4

R(x_0)

\mathrm{{{\to}}E}

2, 5

Q(x_0) \to R(x_0)

\mathrm{{{\to}}I}

4–6

P(x_0) \to (Q(x_0) \to R(x_0))

\mathrm{{{\to}}I}

3–7

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

\mathrm{{\forall}I}

2–8

Lines 3–8 are the first derivation of Proposition 1.4.2 (Section 1.4) at the statements $P(x_0)$ , $Q(x_0)$ , $R(x_0)$ , with line 2 as its premise. The quantifier adds line 2 ( $\mathrm{\forall E}$ at the flag) and line 9 ( $\mathrm{\forall I}$ ), whose side condition holds because the boxes of lines 3 and 4 have closed. About 10 minutes.

Marking scheme. (10 points) 3: the flagged box with $\mathrm{\forall E}$ at the flag. 4: the two $\mathrm{{\to}I}$ boxes in the order of Proposition 1.4.2. 3: the propositional lines named and the side condition of line 9 checked. Fatal error (0): $\mathrm{\forall I}$ written while the box of line 3 or 4 is open.

Exercise (R4)

Derive $\forall x\, \forall y\, (f(x) = y \to g(y) = x) \vdash \forall x\, (g(f(x)) = x)$ .

Solution.

\forall x\, \forall y\, (f(x) = y \to g(y) = x)

x_0

\forall y\, (f(x_0) = y \to g(y) = x_0)

\mathrm{{\forall}E}

f(x_0) = f(x_0) \to g(f(x_0)) = x_0

\mathrm{{\forall}E}

f(x_0) = f(x_0)

\mathrm{{=}I}

g(f(x_0)) = x_0

\mathrm{{{\to}}E}

3, 4

\forall x\, (g(f(x)) = x)

\mathrm{{\forall}I}

2–5

The tools: instantiate at the term you need (Definition 5.3.1, Section 5.3), here the compound term $f(x_0)$ at line 3, and $\mathrm{{=}I}$ (Definition 5.7.1, Section 5.7), which makes the hypothesis of line 3 at no cost. Why the look-alikes fail: $\mathrm{{=}E}$ has no equation to cite, since no line is an equation until $\mathrm{{=}I}$ writes one; $\mathrm{\forall E}$ at a fresh variable $y_0$ leaves the hypothesis $f(x_0) = y_0$ , which nothing proves; and there is no existential, so $\mathrm{\exists E}$ has nothing to open. About 15 minutes.

Marking scheme. (10 points) 2: the flagged box. 4: the second $\mathrm{\forall E}$ , at $f(x_0)$ . 3: $\mathrm{{=}I}$ and $\mathrm{{\to}E}$ . 1: the closing $\mathrm{\forall I}$ with the flag checked. Fatal error (0): $\mathrm{\forall E}$ at a variable $y_0$ followed by a step that treats $f(x_0) = y_0$ as proved.

5.8.1. Unique existence

5.8.2. How uniqueness is used and proved

5.8.3. Counting with equality

5.8.4. The x such that φ

5.8.5. A function symbol and its graph

5.8.6. Definitions add words, not facts

5.8.7. Exercises

A. Check your understanding

B. Practice

C. Going deeper

R. Review

5.8.4. The $x$ such that $\varphi$