Formal structure of a proof with the goal $\exists x P(x)$

Question

In How To Prove It?, Velleman explains that, in order to prove a statement with a goal of the form $\exists x P(x)$, we must declare an arbitrary variable $y$ and assign a value $a$ to it and use the assignment to prove the substitution instance $P(y/x)$ of the goal. Hence, assuming $\Gamma$ is a well-founded formula, we have:

1. $\Gamma \rightarrow \exists x P(x)$
2. $(\Gamma \land (y=a)) \rightarrow P(y/x)$

My question concerns the formal structure of such proof technique and the relation between statements 1 and 2.

My first attempt was this one: since $P(a)$ is logically equivalent to $\forall y[(y=a) \rightarrow P(y)]$, then $\Gamma \rightarrow P(a)$ is equivalent to $\Gamma \rightarrow \forall y[(y=a) \rightarrow P(y)]$. If $y$ does not occur in $\Gamma$, then the last statement is equivalent to $\forall y[\Gamma \rightarrow ((y=a) \rightarrow P(y))]$, which means $\forall y[(\Gamma \land (y=a)) \rightarrow P(y)]$.

Now, since $\Gamma \rightarrow P(a)$ implies $\Gamma \rightarrow \exists x P(x)$, it is fair to believe that the relation between statements 1 and 2 is $\forall y[(\Gamma \land (y=a)) \rightarrow P(y)] \rightarrow [\Gamma \rightarrow \exists x P(x)]$.

However, some members on this site informed me that this implication is a weaker version of the more general assertion $\forall y[[(\Gamma \land (y=a)) \rightarrow P(y)] \rightarrow [\Gamma \rightarrow \exists x P(x)]]$. In this case, $y$ appears as a free variable, whose quantification ranges upon the entire proof. However, I can't tell how it is possible to derive such stronger implication, especially because the formula $(\Gamma \land (y=a)) \rightarrow P(y)$ seems meaningless to me.

Answer 1

IMO, your analysis of Existential Introduction is unnecessarily complicated...

The intuitive reasoning is the following:

if we know that Socrates is a Philosopher, then we are licensed to assert that a Philosopher exists.

In symbols:

$\dfrac { P(s) } { \exists x P(x)}$.

Thus, there is no need to add a "declaration" about the term (i.e. a "name") $s$.

---

Things are different with Existential Elimination, where we have $\exists x P(x)$ as premise.

In this case, we introduce a new term $a$ to "temporary" refer to the unknown individual that we know to exists.

The "new" condition is formalized through the proviso that $a$ must not be used in the "context" $\Gamma$, nor in the conclusion of the proof.

---

---

With ref to Velleman's book, page 112, I do not see big differences...

The author says:

"Try to find a value of $x$ for which you think $P(x)$ will be true."

This amounts to saying: "let $x= \text {Socrates}$".

"... and proceed to prove $P(x)$ for this value of $x$."

This amounts to saying: "prove $\text {Philosopher}(\text {Socrates})$".

Then apply EI to conclude that $\exists x (\text {Philosopher}(x))$.

Answer 2

Suppose you are trying to prove $\exists y(y+2x = 0)$. Here are two ways you might write the proof:

1. Prove $(-2x)+2x=0$.
2. Start with the sentence "Let $y = -2x$" and then prove $y+2x=0$.

The logic of these two approaches is exactly the same; the difference is merely stylistic. In the second approach, the letter $y$ is just being introduced as a notational shorthand for $-2x$.

Which style is better? It may depend on the example, and it may be a matter of taste. But if the conclusion of the theorem being proven has been stated with an explicit existential quantifier, then I think many mathematicians would prefer the second style.

For example, suppose you are giving an $\epsilon$-$\delta$ proof of a limit statement--say, $\lim_{x \to 2} 3x = 6$. The statement to be proven is $\forall \epsilon>0 \exists \delta>0 \forall x(0 < |x-2| < \delta \to |3x-6|<\epsilon)$. I think most mathematicians would start the proof like this: "Let $\epsilon$ be an arbitrary positive number. Let $\delta = \epsilon/3$. Then $\ldots$." There is really no need for the sentence "Let $\delta = \epsilon/3$." One could simply prove that $\epsilon/3$ has the property required for $\delta$, and then conclude that the limit statement is true. But most readers would find the sentence "Let $\delta = \epsilon/3$" helpful, because it tells the reader that $\epsilon/3$ is the number that is being proposed as the value of $\delta$ in the $\epsilon$-$\delta$ definition.

Note that How To Prove It is not a book on formal logic, although there is some logic in the book. It is a book about how to write proofs in English. So although the proof techniques that are discussed often correspond to rules of formal logic, the explanations focus on how to use those techniques to write proofs in English, not how to write proofs in formal logic.