Results 1 to 4 of 4

Math Help - Derivation Error

  1. #1
    Member
    Joined
    Mar 2010
    Posts
    78

    Derivation Error

    Pr1.  \exists x Fx \rightarrow \forall x Gx.

    Pr2.  \forall x (Gx \vee Hx) \rightarrow \forall x Jx.

    C.  \forall x (Fx \rightarrow Jx).


    1. Show \forall x (Fx \rightarrow Jx)

    2. ... Show Fx \rightarrow Jx

    3. ...... Fx ASS CD

    4. ...... Show Jx

    5. ......... \neg Jx ASS ID

    6. ......... \exists x Fx 3 EG

    7. ......... \forall x Gx Pr1 6 MP

    8. ......... Gx 7 UI

    9. ......... Gx \vee Hx 8 ADD

    10. ......... Show \forall x (Gx \vee Hx)

    11. ............ Gx \vee Hx 9 R

    12. ............ 11 UD (ERROR: x appears free in an antecedent line)

    13. ......... \forall x Jx Pr2 10 MP

    14. ......... Jx 13 UI

    15. ......... 5 14 ID

    16. ...... 4 CD

    17. ... 2 UD


    The above is my attempted solution. How do I fix the error at line 12?
    Follow Math Help Forum on Facebook and Google+

  2. #2
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,561
    Thanks
    785

    Re: Derivation Error

    First, you don't need reasoning by contradiction in step 5. The outline of the derivation is the following: you assume Fx is step 3, derive Jx in step 14, close Fx to get Fx -> Jx and introduce the universal quantifier. The assumption 5 has not been used until step 14, and it is not needed after that.

    Concerning step 12, you need to start proving \forall x\, (Gx \vee Hx) before instantiating \forall x\,Gx in step 8. To prove \forall x\, (Gx \vee Hx), you fix some x, instantiate \forall x\,Gx with that x, add the second disjunct and then do universal introduction (UD).
    Follow Math Help Forum on Facebook and Google+

  3. #3
    Member
    Joined
    Mar 2010
    Posts
    78

    Re: Derivation Error

    emakarov, could you please show me how you would prove Ax (Gx v Hx)? I don't quite understand what you mean by "fix some x and instantiate AxGx with that x."

    I have solved the problem using an entirely different method, i.e., quantifier negation, but it would be helpful if you could show me your way.

    Thanks.
    Follow Math Help Forum on Facebook and Google+

  4. #4
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,561
    Thanks
    785

    Re: Derivation Error

    I have not worked with this notation, so the following is probably not completely correct, but it shows the idea.

    Code:
    7.  ......... ∀x Gx Pr1 6 MP
    
    8.  ......... Show ∀x (Gx ∨ Hx)
    
    9.  ............ Show Gx ∨ Hx
    
    10. ............ Gx 7 UI
    
    11. ............ Gx ∨ Hx 8 ADD
    
    12. ......... 11 UD
    
    13. ......... ∀x Jx Pr2 12 MP
    
    etc.
    You proved ∀x Gx in step 7, and now you need to prove ∀x (Gx ∨ Hx) to use Pr2. Currently, there are no suitable objects to instantiate x with in ∀x Gx. When you start proving ∀x (Gx ∨ Hx), you fix some x (the first step in the proof of a universal statement) and with that particular x you instantiate ∀x Gx.
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. Derivation and Jordan derivation
    Posted in the Advanced Algebra Forum
    Replies: 1
    Last Post: May 8th 2011, 10:22 PM
  2. best fit, minimizing point-to-line error, not y error
    Posted in the Advanced Applied Math Forum
    Replies: 1
    Last Post: March 4th 2011, 06:16 AM
  3. Weighted least squared error derivation
    Posted in the Advanced Algebra Forum
    Replies: 1
    Last Post: December 12th 2010, 10:11 PM
  4. Replies: 1
    Last Post: December 10th 2009, 11:48 PM
  5. Replies: 0
    Last Post: April 1st 2009, 05:22 AM

Search Tags


/mathhelpforum @mathhelpforum