# Natural deduction proof of $\forall x (\exists y (P(x) \vee Q(y))) \vdash \exists y (\forall x (P(x) \vee Q(y)))$

I'm trying to do a Fitch proof of

$$\forall x (\exists y (P(x) \vee Q(y))) \vdash \exists y (\forall x (P(x) \vee Q(y)))$$

Edit: using only the axioms on http://www.proofwiki.org/wiki/Category:Natural_Deduction_Axioms, along with universal/existential generalisation/instantiation

The following is my first attempt.

$$\begin{array}{lll} 1 & \begin{array}{l}\forall x (\exists y (P(x) \vee Q(y))) \\ \hline \end{array} & \text{assumption} \\ 2 & \exists y (P(v) \vee Q(y)) & \text{\forallE, 1} \\ 3 & \begin{array}{ll} & \begin{array}{l} P(v) \vee Q(w) \\ \hline\end{array} \end{array} & \text{assumption} \\ 4 & \begin{array}{ll} & \forall x (P(x) \vee Q(w)) \end{array} & \text{\forallI, 3} \\ 5 & \forall x (P(x) \vee Q(w)) & \text{\existsE, 2, 3, 4} \\ 6 & \exists y (\forall x (P(x) \vee Q(y))) & \text{\existsI, 5} \\ \end{array}$$

Edit: I know that this proof is incorrect, since replacing $P(x) \vee Q(y)$ with $R(x, y)$ would yield the result $$\forall x (\exists y (R(x, y)) \vdash \exists y (\forall x (R(x, y))) ,$$ which is clearly not true in general.

I'm not exactly sure on which line the flaw is. I would appreciate it if someone could point that out, and explain why it's wrong.

I suspect that I'm supposed to use the distributivity of $\exists$ over $\vee$ for this one. But I don't know how to formally justify this distributivity, and I can't find a natural deduction proof for it.

Edit: I think I have successfully proved this, based on @ZevChonoles's answer. Here is a screencap:

-
How do you know it's incorrect? Also: Do you distinguish between "Fitch proof" and "natural deduction"? The Wikipedia article for the former looks like it is just an alternative name for a particular typography for natural deduction. – Henning Makholm Jun 17 '12 at 22:04
I don't know which precise rules of inference you have available, but the goal looks like something that needs to be proved by using the rule of excluded middle on $\exists y.Q(y)$ followed by a case analysis. – Henning Makholm Jun 17 '12 at 22:09
In my proof it could have been any R(x, y) rather than P(x) v Q(y). It's surely not true in general that Ax Ey R(x, y) => Ey Ax R(x, y).Sure, any natural deduction proof would do, but I am only familiar with the Fitch typography. – jaakhaamer Jun 17 '12 at 22:10
I'm trying to prove it using only the axioms on proofwiki.org/wiki/Category:Natural_Deduction_Axioms, along with universal/existential generalisation/instantiation. – jaakhaamer Jun 17 '12 at 22:12
Have you got it backwards? Your statement is indeed false, but the converse is true. – Dan Christensen Jun 19 '12 at 4:53

You can't go from step 3 to step 4. For the particular $v$ you chose, you know that you can find $w$ such that $P(v)\vee Q(w)$. If $Q(w)$ is true, then certainly $P(x)\vee Q(w)$ is true for all $x$, but if $Q(w)$ is false there's no reason why it should be the case that $P(x)\vee Q(w)$ for all $x$.

I don't know how to write this in the Fitch format, but the essential idea is just that either $Q(y)$ is true for some $y$, or $Q(y)$ is false for all $y$.

If $Q(v)$ is true for some particular $v$, then $P(x)\vee Q(v)$ is true for all $x$, and so we certainly have that $\exists y(\forall x(P(x)\vee Q(y)))$; the $y$ that exists is just $y=v$.

If $Q(y)$ is false for all $y$, then $P(x)\vee Q(y)\iff P(x)$, so $\forall x(\exists y(P(x)\vee Q(y)))$ implies that $P(x)$ is true for all $x$, and hence $\exists y(\forall x(P(x)\vee Q(y)))$; any $y$ at all will work.

-
Is the $v$ in line 3 necessarily a fixed variable? I was trying to use an arbitrary free variable there, so that I could perform $\forall$-introduction on the next line. – jaakhaamer Jun 17 '12 at 22:21
I'm not actually familiar with formal logic terminology, but I assumed you chose a specific $v$. Your assumption states that for any particular $x$ you choose, you can find a $y$ such that $P(x)\vee Q(y)$; but that the finding of this $y$ is done after choosing the $x$, and therefore the $y$ might depend on the $x$. – Zev Chonoles Jun 17 '12 at 22:27
@jaakhaamer: I've added to my answer. – Zev Chonoles Jun 17 '12 at 22:37
Generalization rules in FOL usually have side conditions to ensure this doesn't happen. There's a bit of variability in exactly how they're formalized, and they can have something of an action-at-a-distance feel in environment-less natural deduction, where you need to require that the generalized variable is not used in any still-open assumption. In the system used here it looks as if there also needs to be explicit conditions on $\exists$-elimination. (But it's not quite clear to me from the example how the rule being used works). – Henning Makholm Jun 17 '12 at 22:51
@Henning, I'm afraid I don't understand your comment; perhaps I shouldn't have answered so quickly in a subject I'm unfamiliar with, since I don't know if what I'm saying is really true (or at any rate, in what contexts it's true). Should I delete my post? – Zev Chonoles Jun 17 '12 at 22:57

Universal introduction has the condition that the name letter generalized upon, cannot occur in any assumption still in effect (equivalently, can't occur in any assumption in the assumption set). It doesn't matter if they appeared anywhere else, the rule only says that they can't appear in any assumption still in effect. At step 3 you have the name letters "v" and "w". So, can't generalize on v to get to line 4. This behaves just like the following:

1 | (Fa $\lor$ Gb) assumption

2 | $\forall$x(Fx $\lor$ Gb) 1 universal introduction (invalid!)

3 ((Fa $\lor$ Gb)$\implies$$\forall$x(Fx $\lor$ Gb)) 1-2 conditional introduction

-

Like many beginners, the OP seems to be having some trouble tracking dependencies among variables -- dependencies that are created by existential specification (eliminate $\exists$) or some equivalent rule. Such dependencies never seem to be an issue in mathematics textbooks. Here is a simple alternative to tracking these dependencies that it seems most authors of mathematics textbooks follow instinctively:

1. Introduce free variables only by a premise or existential specification (eliminate $\exists$).

2. The conclusion to every premise should not contain any free variables introduced in the premise or in any subsequent statement. The conclusion may require some universal or existential generalizations to get rid of any "new" free variables. (Do existential generalizations (introduce $\exists$) before generating conclusion.)

This is not a new form of logic. Rather, it can be seen as a set of guidelines for writing formal mathematical proofs analogous to structured programming guidelines in CS.

Example using DC Proof 2.0 at http://www.dcproof.com/ConclusionExample.htm

-