# $\exists$- introduction rule

My reference is "A Course on Mathematical Logic" by S.M. Srivastava.

This question is about a certain inference rule for proofs in first order logic. If $L$ is a first order language and $T$ is a theory written in $L$, you define a proof in $T$ to be a finite string of formulas $A_1,\dots,A_n$ such that each of the $A_i$ is either a logical axiom (like $\neg A\vee A$ for any forumla $A$), a non-logical axiom (a formula of $T$, an 'axiom' of $T$) or obtained from one or more of the $A_1,\dots,A_{i-1}$ by one of the rules of inference listed in the book. One such rule is the 'intuitive' expansion rule which states that if you've written down $A$ in your proof, and $B$ is any formula you like, you are allowed to write down $B\vee A$.

There is one such rule that I don't quite understand, the $\exists$-introduction rule : if you have already written down $A\rightarrow B$, and $x$ is a variable that is not free in $B$, then you can write down $\exists x A\rightarrow B$.

There is a little ambiguity, but I believe what is meant is $(\exists x A)\rightarrow B$.

What is the meaning of this? Can it be motivated by concrete examples? Why is it 'true'?

-
I'm confused. You talk about an $\exists$-introduction rule but that's not what you have written down. Are you sure that's what the book says? –  Zhen Lin Aug 6 '11 at 8:36
@Zhen Lin you are right, thanks for noticing! –  Olivier Bégassat Aug 6 '11 at 8:46

I call the rule you are talking about existential instantiation. It captures the following idea: suppose you want to prove $q$, which does not depend on $x$, but in order to do so, you need to assume $p(x)$, which does depend on $x$. Then, as long as there is some $x$ such that $p(x)$ holds, $q$ is true, and it doesn't matter what that $x$ is: in other words, $(\exists x . \, p(x)) \to q$.

Here is a simple example. Let $q(y)$ be the proposition ‘$y$ is a non-empty set’. Let $p(x, y)$ be the proposition $x \in y$. Then, it is evident that $p(x, y) \to q(y)$. But $q(y)$ does not depend on $x$, so we may deduce that $(\exists x . \, p(x, y)) \to q(y)$.

But perhaps you prefer some elementary number theory. So let $q(y)$ be the proposition ‘$y \ne 1$ and $y$ is composite’. Let $p(x, y)$ be the proposition ‘$x \ne 1$ and $x \ne y$ and $x$ divides $y$’. Then certainly $p(x, y) \to q(y)$, so $(\exists x . \, p(x, y)) \to q(y)$.

-
Oh, I see! Thanks :) –  Olivier Bégassat Aug 6 '11 at 9:01
Can you maybe shed some light as to why we want $x$ not to be free within $q$? –  Olivier Bégassat Aug 6 '11 at 9:03
Heuristically, this is because $\exists x$ binds $x$, so it is no longer meaningful in context. Concretely, let $q(x)$ be the proposition $x = 1$, and $p(x)$ be the proposition $x = 1$. Then obviously $p(x) \to q(x)$, but it is certainly not true that $(\exists x . \, p(x)) \to q(x)$. I believe a neater presentation, without invoking variable names or the free/bound distinction, is possible, but I have not found one myself. –  Zhen Lin Aug 6 '11 at 9:10

Following Zhen Lin's Example , you must take in account that inference rules mut be sound, i.e. for every interpretation of the language, if the premisses of the rule are true in that interpretation, so also is the conclusion.

Take the $\exists$-intro rule : if $A(x) \rightarrow B$ then $\exists xA(x) \rightarrow B$ , and remove the restriction on $x$ being free in $B$.

Let your interpretation having domain the set of natural nambers and let $E()$ a predicate constant of your language standing for "$x$ is Even".

Consider the formula : $E(x) \rightarrow \lnot x = 1$ and "interpret" it, i.e. consider an assignement of objects of the domain (numbers) to the free variables in your formula (the $x$).

If the value assigned to $x$ is $1$, then Even$(1)$ is false, and so the conditional is true.

If the value assigned to $x$ is a number $n$ different from $1$, then $\lnot n = 1$ is true, and again the conditional is true.

So, in this interpretation, the formula is always true.

What happens with the conclusion ? It is now : $\exists xE(x) \rightarrow \lnot x = 1$.

Of course, $\exists xE(x)$ is true, because there are even numbers, but the number $1$ is not different from itself; so $\exists xE(x) \rightarrow \lnot x = 1$ is not always true in this interpretation .

Conclusion : the rule stated without restriction on free vars would license false conclusion from true premisses, i.e. is not sound.

-