# Derivation using Fitch

• Oct 22nd 2011, 02:53 PM
Lepzed
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!
• Oct 22nd 2011, 03:29 PM
emakarov
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.
• Oct 23rd 2011, 03:07 AM
Lepzed
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)```