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

Hi guys. I came up with a "proof" for , where is a prime formula, which is obviously false. But what have I done wrong?

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

Suppose is a prime formula. Then

(1) - premise
(2) - generalization (Church *301, §30).

Therefore . By the deduction theorem (Church *360, §36), it follows that . So

(3) - theorem (from above)
(4) - axiom (Church *304, §30)
(5) - 3,4,mp
(6) - 5, def. of
(7) - 6, equ. of
(8) - premise
(9) - 7,8,mp
(10) - 9, generalization (Church *301, §30)
(11) - axiom (Church *306, §30)
(12) - 10,11,mp
(13) - 12, generalization (Church *301, §30).

So , which by the deduction theorem (Church *360, §36) means . But clearly this is false! So where did I go wrong?

Thanks in advance!

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!

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