Results 1 to 3 of 3

Math Help - Strange pure predicate calculus result, what went wrong?

  1. #1
    Senior Member
    Joined
    Feb 2008
    Posts
    410

    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!
    Follow Math Help Forum on Facebook and Google+

  2. #2
    Senior Member
    Joined
    Feb 2008
    Posts
    410
    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!
    Follow Math Help Forum on Facebook and Google+

  3. #3
    Senior Member
    Joined
    Feb 2010
    Posts
    466
    Thanks
    4
    That might be the best way to learn. Make the mistake in real live time, then you really see the importance of the prohibition.
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. derivations in predicate calculus
    Posted in the Discrete Math Forum
    Replies: 4
    Last Post: April 23rd 2010, 07:44 AM
  2. predicate calculus
    Posted in the Discrete Math Forum
    Replies: 8
    Last Post: December 13th 2009, 11:01 AM
  3. Predicate calculus - propositions
    Posted in the Discrete Math Forum
    Replies: 3
    Last Post: August 2nd 2009, 08:50 PM
  4. Predicate Calculus
    Posted in the Calculus Forum
    Replies: 1
    Last Post: May 21st 2009, 05:19 PM
  5. Predicate Calculus help
    Posted in the Discrete Math Forum
    Replies: 5
    Last Post: March 6th 2009, 10:19 PM

/mathhelpforum @mathhelpforum