Existential Elimination
Introduction
Existential Elimination $(\existsE)$ is one of the more cryptic rules of modern logic, but many important and even rudimentary proofs in mathematics depend on it. Let’s demystify this rule with such an example, and hopefully, improve our skill reading and writing proofs along the way. Our case in point will be the following elementary theorem from algebra.
Equivalence Relations and Partitions
If $\sim$ is an equivalence relation on a set $S,$ then the set of equivalence classes of $\sim$ forms a partition of $S.$ (Durbin 51)
Before we dive in on this proof, let us review
the focus of our interest.
Existential Elimination
For ease of reference, the rule is repeated below using a Fitch diagram. Although our study will focus on an example of its application “in the wild”, (the previous proof), those interested are invited to read (Bergmann 452) for a more complete description of the rule than what is given here. In what follows, $\mathscr{P}$ and $\mathscr{Q}$ are arbitrary propositions and $\mathscr{P}(a/x)$ is the same as $\mathscr{P}$ but with all occurrences of $x$ replaced by $a.$
Existential Elimination $(\exists\text{E})$
$(\exists x)\mathscr{P}$ | ||
$\mathscr{P}(a/x)$ | ||
$\mathscr{Q}$ | ||
$\rhd$ | $\mathscr{Q}$ |
- $a$ does not occur in an undischarged assumption.
- $a$ does not occur in $(\exists x)\mathscr{P}.$
- $a$ does not occur in $\mathscr{Q}.$
Other Considerations
The proof exhibits other features which the uninitiated may find difficult to follow. In this section I provide some additional material that will help to explain those features in passing, but they will not be the primary focus. Instead, further reading will be indicated.
If $A$ and $B$ are sets, then $A$ is a subset of $B$ if every element of $A$ is an element of $B$. In symbols:We may also write $B\supseteq A$ to indicate $A\subseteq B.$
If $(\forall x)(x\in A \Rightarrow x\in B)$ then $A\subseteq B.$ (Gaughan 2)
If $A$ and $B$ are sets, then $A=B$ if $A\subseteq B$ and $B\subseteq A.$ (Gaughan 3)
$\mathscr{P}(a)$ if and only if $a\in \{x\mid \mathscr{P}(x)\}.$
If $\mathcal{P}$ is a collection of subsets of $S$ then \( \cup\mathcal{P} =\{x\mid\exists y \in\mathcal{P}:x\in y\}. \) (Enderton 3)For example, if $\mathcal{P}=\{A_1,\ldots,A_n\}$ for some $n$ and $A_i\subseteq S$ for each $i=1\ldots n,$ then we show that $x\in\cup\mathcal{P}$ by showing that $x\in A_i$ for some $A_i\in\mathcal{P}.$
A relation $\sim$ on a nonempty set $S$ is anequivalence relation on $S$ if it satisfies the following three properties:(Durbin 49)
- Reflexive. If $a\in S$ then $a\sim a.$
- Symmetric. If $a,b\in S$ and $a\sim b$ then $b\sim a.$
- Transitive. If $a,b,c\in S$ and $a\sim b$ and $b\sim c$ then $a\sim c.$
Let $\sim$ be an equivalence relation on a set $S,$ let $a\in S,$ and let $\class{a}=\{x\in S\mid a\sim x\}.$ This subset $\class{a}$ of $S$ is called the equivalence class of $a$ (relative toIt follows immediately that $a\sim b$ iff $\class{a}=\class{b}.$$\sim$). (Durbin 51)
A collection $\mathcal{P}$ of nonempty subsets of a nonempty set $S$ forms apartition of $S$ provided(Durbin 50)
- $S$ is the union of the sets in $\mathcal{P},$ and
- if $A$ and $B$ are in $\mathcal{P}$ and $A\ne B,$ then $A\cap B=\varnothing.$
Dissecting the Proof
To study the proof generally and how it uses $\existsE$ in particular, let us re-write it in a Fitch diagram.
1 | \( (\forall x\in S)(x\sim x) \) | as | ||||
2 | \( (\forall x,y\in S)(x\sim y \Rightarrow y\sim x) \) | as | ||||
3 | \( (\forall x,y,z\in S)(x\sim y\land y\sim z\Rightarrow x\sim z) \) | as | ||||
4 | \( \mathcal{P}=\{\class{x}\mid x\in S\} \) | as | ||||
5 | \( a\in S \) | as | ||||
6 | \( a\sim a \) | 1 $\forallE$ | ||||
7 | \( a\in\class{a} \) | 6 df $\class{a}$ | ||||
8 | \( (\exists x\in\mathcal{P}) (a\in x) \) | 7 $\existsI$ | ||||
9 | \( a\in\cup P \) | 8 | ||||
10 | \( a\in S\Rightarrow a\in\cup P \) | 5-9 $\Rightarrow\text{I}$ | ||||
11 | \( a\in\cup\mathcal{P} \) | as | ||||
12 | \( (\exists x)(a\in\class{x}\land x\in S) \) | 11 df $\cup P$ | ||||
13 | \( a\in\class{x}\land x\in S \) | as | ||||
14 | \( a\in\class{x} \) | 13 $\land\text{E}$ | ||||
15 | \( a\in\{y\mid y\sim x\land y\in S\} \) | 14 df $\class{x}$ | ||||
16 | \( a\sim x\land a\in S \) | 15 $\{x\mid\mathscr{P}(x)\}\text{E}$ | ||||
17 | \( a\in S \) | 16 $\land\text{E}$ | ||||
18 | \( a\in S \) | 12, 13-17 $\existsE$ | ||||
19 | \( a\in\cup P \Rightarrow a\in S \) | 11-18$\Rightarrow\text{I}$ | ||||
20 | \( S\subseteq\cup P \) | 10 df $\subseteq$ | ||||
21 | \( \cup P\subseteq S \) | 19 df $\subseteq$ | ||||
22 | \( S=\cup\mathcal{P} \) | 20, 21 $=I$ | ||||
23 | \( \class{a}\cap\class{b}\ne\varnothing \) | as | ||||
24 | \( (\exists x)(x\in\class{a}\cap\class{b}) \) | 23 $\existsI$ | ||||
25 | \( c\in\class{a}\cap\class{b} \) | as | ||||
26 | \( c\in\class{a} \) | 25 $\cap\text{E}$ | ||||
27 | \( c\in\class{b} \) | 25 $\cap\text{E}$ | ||||
28 | $x\in\class{a}$ | as | ||||
29 | $a\sim c$ | 26 df $\class{x}$ | ||||
30 | $a\sim x$ | 28 df $\class{x}$ | ||||
31 | $c\sim a$ | 2, 29 | ||||
32 | $c\sim x$ | 3, 30, 31 | ||||
33 | $b\sim c$ | 27 df $\class{x}$ | ||||
34 | $b\sim x$ | 3, 32, 33 | ||||
35 | $x\in\class{b}$ | 34 df $\class{x}$ | ||||
36 | \( x\in\class{a}\Rightarrow x\in\class{b} \) | 28-35 $\Rightarrow\text{I}$ | ||||
37 | \( (\forall x) (x\in\class{a}\Rightarrow x\in\class{b}) \) | 36 $\forallI$ | ||||
38 | \( \class{a}\subseteq\class{b} \) | 37 $\subseteq\text{I}$ | ||||
39 | \( \class{b}\subseteq\class{a} \) | 28-38 R (a/b, b/a) | ||||
40 | $\class{a}=\class{b}$ | 38, 39 $=\text{I}$ | ||||
41 | $\class{a}=\class{b}$ | 24, 25-40 $\existsE$ | ||||
42 | \( \class{a}\cap\class{b}\ne\varnothing \Rightarrow \class{a}=\class{b} \) | 23-41 $\Rightarrow\text{I}$ | ||||
43 | \( \class{a}\ne\class{b} \Rightarrow \class{a}\cap\class{b}=\varnothing \) | 42 Trans | ||||
44 | QED | 1-43 $\Rightarrow\text{I}$ |
In the original proof, Existential Elimination is needed twice, visible in the Fitch version on lines 18 and 41. These lines in turn refer to the relevant blocks needed to apply the $\existsE$ rule as defined previously.
As you compare, you will notice that the original proof is far less explicit about many of the steps, though they are suggested or implied. This is typical of proofs in the mathematical literature. An effective way to learn the abbreviated forms is to learn what is being abbreviated. Fitch diagrams can help with that endeavor. Otherwise, reading and writing proofs can become a mindless parroting exercise of memorization, defeating their purpose to gain an intuition and confidence around the truth of theorems. Learn the rules and they will fade into the background. It’s not the only way, but it’s one I recommend.
Works Cited
Bergmann, Merrie, James Moor and Jack Nelson. The Logic Book. Third Edition. New York: McGraw Hill. 1998. Print.
Durbin, John R. Modern Algebra, An Introduction. Fourth Edition. New York: John Wiley & Sons, Inc. 2000. Print.
Enderton, Herbert B. A Mathematical Introduction to Logic. Second Edition. Burlington: Harcourt/Academic Press, 2001, 1972. Print.
Gaughan, Edward D. Introduction to Analysis. Fifth Edition. Providence: American Mathematical Society, 1998. Print.