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.

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)