Results 1 to 3 of 3

Math Help - Derivation using Fitch

  1. #1
    Junior Member
    Joined
    Jul 2011
    Posts
    53

    Derivation using Fitch

    I'm working on some problems on natural deduction, sadly I'm stuck with this one.
    In our system we're allowed to rewrite P v Q to ~P => Q, '~' represents the 'not' connective:

    Code:
    Show that: (P <=> Q) => ((P ^ Q) v (~P ^ ~Q))
    
    (P => Q) ^ (Q => P)                             [ 1: H]
        ~(P ^ Q)                                    [ 2: H]
    
            ~P                                      [ C - 4: ?
            ~Q                                      [ C - 3: ?
    
        ~P ^ ~Q
        ~(P ^ Q) => (~P ^ ~Q)                       [ C - 2: =>I  2, C - 3]
        (P ^ Q) v (~P ^ ~Q)                         [ C - 1: v, C - 2]
    (P <=> Q) => ((P ^ Q) v (~P ^ ~Q))              [ C: => 1, C-1]
    I keep getting stuck between 2 and C - 2, and basically I'm not sure if I should eliminate the ^ in the first hypotheses. My intuition tells me I've to work something in with RAA, but I can't seem to figure out what and how. Any help would be, again, greatly appreciated!
    Follow Math Help Forum on Facebook and Google+

  2. #2
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,502
    Thanks
    765

    Re: Derivation using Fitch

    The first thing that comes to mind is to convert P => Q into ~P \/ Q and Q => P into ~Q \/ P and then use disjunction elimination rule to consider all four combinations: ~P and ~Q, ~P and P, Q and ~Q, Q and P. The second and third combinations imply contradiction, from which you can derive anything, including P /\ Q \/ ~P /\ ~Q.
    Follow Math Help Forum on Facebook and Google+

  3. #3
    Junior Member
    Joined
    Jul 2011
    Posts
    53

    Re: Derivation using Fitch

    Hmm, ex falso isn't part of this method, we're supposed to solve disjunction by rewriting it to an implication.
    Which brings me to my next question:

    Code:
    Derive: ((P => Q) => ~P) => (P => ~Q)
    (P => Q) => ~P                                       [ 1, H]
        P                                                [ 2, H]
            Q                                            [ 3, H]
    {Now, I've to conclude false from Q. I have  both a P and a ~P in my premiss, 
    from which I can derive a contradiction.
    But, how am I allowed to eliminate the ~P from 1? 
    Since I have both P and Q assumed I would say I actually have  P => Q, 
    on the other hand, introducing the => means I;ve to end the assumption 'Q'.
    ^-Intro isn't useful either? Or is it possible to eliminate 
    the P=>Q on the basis that P ^ Q is a stronger proposition than P=>Q? 
    I know I've to 'get' the ~P, but I'm not sure by which rule I'm allowed to do this.}
    
    { One possibility I've explored is this: }
                P => Q      [H]
                    ~P         [ =>E 1]
                    False      [Contradiction P, ~P]
               ~(P => Q)   [False Intro on P => Q and False]
                False         [Contradiction P=>Q, ~(P =>Q), but is this allowed???]
            ~Q
        P => ~Q
    ((P => Q) => ~P) => (P => ~Q)
    Last edited by Lepzed; October 23rd 2011 at 03:29 AM.
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. Replies: 9
    Last Post: December 10th 2011, 01:23 PM
  2. Abstract reasoning/natural deduction with Fitch
    Posted in the Discrete Math Forum
    Replies: 10
    Last Post: October 19th 2011, 12:37 PM
  3. Derivation and Jordan derivation
    Posted in the Advanced Algebra Forum
    Replies: 1
    Last Post: May 8th 2011, 09:22 PM
  4. How to convert with Fitch ~A v B to A -> B ?
    Posted in the Discrete Math Forum
    Replies: 7
    Last Post: June 30th 2010, 03:45 AM
  5. Formal proof (using Fitch Format) with an OR
    Posted in the Discrete Math Forum
    Replies: 5
    Last Post: June 29th 2010, 02:06 AM

Search Tags


/mathhelpforum @mathhelpforum