Since you did not edit your post to add a note that it has been solved, was the [SOLVED] tag added intentionally?
Thanks. I found a solution
Only the last item leaves me wrong, for example: ~ pI goal ~ q ~ (p ^ q) - I can do up to 17, then later I got wrongI do not know why? Maybe I do not understand something. From the pictures that I have noted: 1, 2-9, 10 -17 and or eliminations. - Only 18 leaves me wrong: (
Does "I" mean disjunction, i.e., "or"? Usually it is denoted by ∨. In ASCII one can also write \/ or the letter "v".
By "last", do you mean number 3 in the quote above?
This is hard to understand. I am not sure what "pI" is and why there is no connective between "~q" and "~(p ^ q)".
This is also hard to understand without seeing the first 17 steps.
1.~p | ~q Premise
2.~p Assumption
3.p & q Assumption
4.p And Elimination: 3
5.p & q => p Implication Introduction: 4
6.~p Reiteration: 2
7.p & q Assumption
8.~p Reiteration: 6
9.p & q => ~p Implication Introduction: 8
10.~(p & q) Negation Introduction: 5, 9
11.~p => ~(p & q) Implication Introduction: 10
12.~q Assumption
13.p & q Assumption
14.q And Elimination: 13
15.p & q => q Implication Introduction: 14
16.p & q Assumption
17.~q Reiteration: 12
18.p & q => ~q Implication Introduction: 17
19.~(p & q) Negation Introduction: 15, 18
20.~q => ~(p & q) Implication Introduction: 19
21.~(p & q) Or Elimination: 1, 11, 20
This is the solution I got. But it's too long.
Still it works
I believe this is the correct derivation. I don't see how it can be shortened except by removing step 6 and making step 8 a reiteration of 2.
A more standard variant of natural deduction (of which Fitch calculus is a particular notation) has a symbol ⊥ for contradiction. Then negation introduction is shorter: you assume ~p and p & q, derive p, derive ⊥ from ~p and p, then close the assumption p & q and derive ~(p & q) in one step. There is no need to derive p & q => p and p & q => ~p. Similarly, or elimination does not require implications ~p => ~(p & q) and ~q => ~(p & q): you just derive ~(p & q) two times from assumptions ~p and ~q, respectively, and or elimination derives ~(p & q) and closes the ~p and ~q in one step.
We have a premise ~(p & q). The proof of ~p | ~q is by contradiction, i.e., we assume ~(~p | ~q) and prove p & q (described below), which contradicts the premise. This gives ~~(~p | ~q) by negation introduction and then ~p | ~q by negation elimination.
So, assume ~(~p | ~q). We need to prove p and q. These two subderivations are similar. To prove p, we assume ~p and derive ~p | ~q, which contradicts the assumption. Therefore, ~~p and we conclude p by negation elimination. The second part, q, is proved similarly.
hi emakarov
I'm struggling with this one still ...
this is what I have so far:
1. ~(p & q) Premise
2. ~(~p | ~q) Assumption
3. ~p Assumption
4. ~p | ~q Or Introduction: 3
5. ~p => ~p | ~q Implication Introduction: 4
6. ~p Assumption
Now I'm stuck as to how to get to the conclusion of ~p|~q.
Can you please help?
Also ... please bear in mind I don't have the necessary background in discrete mathematics .. so is there a specific textbook or site you can recommend also so I can understand better and learn?
Thank you so much in advance