~(P /\ Q) |- Q -> ~P
I don't know where to start. Negation confuses me.
I have to solve this in Isabelle (a program), but if someone explains how to solve using natural deduction, it will be enough help.
This is an example that the quality of an SO question is many times determined by an answer, not the question. I kind of give this answer to thank M.Eberl for another useful answer, since I can't make comments.
As to a comment above, that you may be asking a homework question, the comment is valid, but if you're confused by negation, then you're mostly doomed anyway, until you make progress, so even one complete answer wouldn't help you, and here, there's no right answer.
The formula is so basic, except through applying step-by-step rules, it would be hard for anyone to prove that they understand what they're proved, without going through the multitude of tedious steps to do so.
For example:
lemma "~(P ∧ Q) ==> Q --> ~P"
by auto
Surely that gets you nothing, if the requirement is that you demonstrate understanding.
I've largely made progress "by the method of absorption over time", and in his answer, M.Eberl gave a significant outline of the basics of natural deduction. My interest in it was to mess around and see if I could absorb a little more.
As to rule and erule, there is the cheat sheet:
As to the proof of logic by means of Isabelle, Isabelle/HOL is so big and involved, that a little help, once, doesn't get you much, though collectively, it's all important.
I learned long ago the equivalent statement of an implication. It's even in HOL.thy, line 998:
lemma disj_not2: "(P | ~Q) = (Q --> P)"
From that, it's easy to see, along with DeMorgon's laws (line 993 of HOL.thy), that you stated an equivalency in your question.
Well, of course, not quite, and that's where all the hassle comes in. Rearranging things, based on trivial equivalencies, to finally prove the equivalency. (While also knowing what the notation means, such as that your |- will be ==>. I use ASCII because I don't trust the graphical in browsers.)
M.Eberl mentioned structured proofs. Consider this one:
lemma "~(P ∧ Q) ==> Q --> ~P"
proof-
fix P Q :: bool
assume "~(P ∧ Q)"
hence "~P ∨ ~Q" by simp
hence "~Q ∨ ~P" by metis
thus "Q --> ~P" by metis
qed
What would I deserve in points, for homework? Nothing much. It's actually a testimony that metis knows how to use basic first-order logic. Otherwise, how did it know to make the jump from ~Q ∨ ~P to Q --> ~P?