# Thread: Derivation using Fitch

1. ## 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!

2. ## 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.

3. ## 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)