NEW QUESTION about Fitch

Quote:

---

Originally Posted by rai009

Given ¬(p∧q), use the Fitch system to prove (¬p∨¬q)

---

This is a little trickier and requires the use of negation elimination, which is properly called double-negation elimination. It is easier to derive (¬p ∨ ¬q) if you can derive (A ∨¬A) for any formula A. But assuming this is not done, we proceed as follows.

Assume ¬(¬p ∨ ¬q). From this in the end we will derive a contradiction and thus ¬¬(¬p ∨ ¬q), and then use double-negation elimination to derive (¬p ∨ ¬q). Now assume p and q. Then p ∧ q, which contradicts ¬(p ∧ q). Therefore, ¬p, which implies (¬p ∨ ¬q). This in turn contradicts ¬(¬p ∨ ¬q), so we conclude ¬q. Then we repeat by deriving (¬p ∨ ¬q), which again contradicts ¬(¬p ∨ ¬q). Thus, ¬¬(¬p ∨ ¬q) and (¬p ∨ ¬q).

Thanks for the help but i can't show contradiction as i mentioned before my program doesn't allow contradiction introduction.....how do i do it without using contradiction introduction rule?

You can read the word "contradiction" informally. In the description in post #16, contradiction is derived from A and ~A for some formula A, and this contradiction is immediately used to close one of the open assumption and derive the negation of that assumption. In your case, you derive the negation of the assumption directly from A and ~A.