# Does existential elimination affect whether you can do a universal introduction?

In exercise 1 of http://cnx.org/content/m10774/latest/, it says that you cannot do the universal introduction in

1   ∀y:(∃x:(R(x,y)))    Premise
2   ∃x:(R(x,q))         ∀Elim, line 1
3   R(p,q)              ∃Elim, line 2
4   ∀y:(R(p,y))         ∀Intro, line 3


because the existential elimination introduces the proxy variable p which could depend on the arbitrary variable q and hence q might no longer be arbitrary.

Does this make sense? If so, can you come up with examples of when this is the case?

-
What do you understand by ∃Elim? The rule as I know it does not permit the inference of line 3 from line 2. (For reference: I understand ∃Elim to be the rule of inference which allows one to infer $q$ from $\exists x. p(x)$ and $p(x) \rightarrow q$, where $x$ does not appear in $q$.) –  Zhen Lin Jun 7 '11 at 19:19

Take the universe to be the real numbers $R(x,y)$ to mean "$x\lt y$". Then the presmise says that for every real number $y$, there is a real number $x$ that is strictly smaller than $y$. This is true.

Line two eliminates the universal quantifier, and says that there is a real numbers $x$ which is smaller than $q$ ($q$ an unspecified, but fixed, real number). This is still true, regardless of what $q$ is. Say $q=1$.

Line 3 then eliminates the existential by selecting a specific $p$ which is smaller than $q$. This is still true; say, $p=0$.

Line 4 is now false: it would say "for every real number $y$, $0\lt y$. This is invalid.

The problem is that the $p$ introduced in line $3$ may depend on the $q$ introduced on line 2; it is not arbitrary and independent, so when you try introducing the universal quantifier in place of $q$, you are implicitly affecting $p$ as well.

-
So which restriction in universal introduction solves this issue? –  mtanti Jun 7 '11 at 18:55
@mtanti: So you must restrict universal introduction somehow, lest you cause this kind of problem. –  Arturo Magidin Jun 7 '11 at 18:57
@mtanti: here's the restriction you're looking for, from the web page you cite: "A variable is not arbitrary if it is free after applying [Existential] Elim -- either as the introduced witness, or free anywhere else in the formula." –  ShyPerson Jun 10 '11 at 21:35

We introduce a bit of romance. Let $R(x,y)$ mean that $x$ loves $y$. And let us assume, that as the old song says, everyone has someone who loves him/her (this is the first line). Actually, we can be unromantic and not quite believe it, since we are merely deducing consequences from it.

Take a particular individual $q$. The second line says that someone loves $q$. This clearly follows from the first line.

Call one of the people who loves $q$ by the name $p$. That gives us the third line.

Does $p$ love everybody? (The fourth line asserts that (s)he does.) Possible, but rather unlikely. Anyway, it is certainly not deducible from the fact that $p$ loves $q$.

Or if romance is not your style, what about biology? Let $R(x,y)$ mean that $x$ is the mother of $y$. The first line says that everybody has a mother. In the next few lines we try to deduce consequences.

The second and third lines follow easily, as in the "loves" case. So $p$ is the mother of $q$. Surely we cannot deduce in the fourth line that $p$ is everyone's mother.

-