# 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?