# 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 $\displaystyle \vdash(\exists x)Ax\to (y)Ay$, where $\displaystyle 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, $\displaystyle F^1$ (found in §30).

Suppose $\displaystyle Ax$ is a prime formula. Then

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

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

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

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