# Thread: Strange pure predicate calculus result, what went wrong?

1. ## Strange pure predicate calculus result, what went wrong?

Hi guys. I came up with a "proof" for $\vdash(\exists x)Ax\to (y)Ay$, where $Ax$ is a prime formula, which is obviously false. But what have I done wrong?

I'm using Church's first pure predicate calculus formulation, $F^1$ (found in §30).

Suppose $Ax$ is a prime formula. Then

(1) $\neg Ax$ - premise
(2) $(x)\neg Ax$ - generalization (Church *301, §30).

Therefore $\neg Ax\vdash (x)\neg Ax$. By the deduction theorem (Church *360, §36), it follows that $\vdash (\neg Ax)\to(x)\neg Ax$. So

(3) $(\neg Ax)\to(x)\neg Ax$ - theorem (from above)
(4) $((\neg Ax)\to (x)\neg Ax)\to((\neg(x)\neg Ax)\to\neg \neg Ax)$ - axiom (Church *304, §30)
(5) $(\neg(x)\neg Ax)\to\neg \neg Ax$ - 3,4,mp
(6) $((\exists x) Ax)\to\neg \neg Ax$ - 5, def. of $\exists$
(7) $((\exists x) Ax)\to Ax$ - 6, equ. of $\neg\neg$
(8) $(\exists x) Ax$ - premise
(9) $Ax$ - 7,8,mp
(10) $(x)Ax$ - 9, generalization (Church *301, §30)
(11) $(x)Ax\to Ay$ - axiom (Church *306, §30)
(12) $Ay$ - 10,11,mp
(13) $(y)Ay$ - 12, generalization (Church *301, §30).

So $(\exists x)Ax\vdash(y)Ay$, which by the deduction theorem (Church *360, §36) means $\vdash(\exists x)Ax\to (y)Ay$. But clearly this is false! So where did I go wrong?

Thanks in advance!

2. Okay, looks like I discovered what precisely went wrong. Apparently when using premises (as opposed to axioms) in the proof, we are not allowed to generalize on free variables in those premises. So, steps (2) and (10) are illegal. That was unexpected! I suppose I should read the textbook more carefully next time...

Thanks anyway guys!

3. That might be the best way to learn. Make the mistake in real live time, then you really see the importance of the prohibition.