1. ## Fitch :(

Hi.

How to prove:
1.p=>q - permission goal ~q=>~p
2. ~p=>q - permission and q=>r goal (~p=>~r)=>p
3. ~pI~q goal ~(p^q)

Thanks

2. ## Re: Fitch :(

Since you did not edit your post to add a note that it has been solved, was the [SOLVED] tag added intentionally?

3. ## Re: Fitch :(

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: (

4. ## Re: Fitch :(

Originally Posted by anastazya
3. ~pI~q goal ~(p^q)
Does "I" mean disjunction, i.e., "or"? Usually it is denoted by ∨. In ASCII one can also write \/ or the letter "v".

Originally Posted by anastazya
Only the last item leaves me wrong
By "last", do you mean number 3 in the quote above?

Originally Posted by anastazya
for example: ~ pI goal ~ q ~ (p ^ q)
This is hard to understand. I am not sure what "pI" is and why there is no connective between "~q" and "~(p ^ q)".

Originally Posted by anastazya
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: (
This is also hard to understand without seeing the first 17 steps.

5. ## Re: Fitch :(

do u mean
premise ~p|~q
to prove ~(p&q)???

I'm also looking for the proof of this.

6. ## Re: Fitch :(

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

7. ## Re: Fitch :(

Originally Posted by Thejanie
This is the solution I got. But it's too long.
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.

8. ## Re: Fitch :(

The program I used doesn,t have contradiction. BTW can you help me to prove this the other way around? I mean starting from ~(p & q) as the premise to prove ~p | ~q.

9. ## Re: Fitch :(

Originally Posted by Thejanie
BTW can you help me to prove this the other way around? I mean starting from ~(p & q) as the premise to prove ~p | ~q.
Ah, this is more complicated. This requires the rule of double-negation elimination or the law of excluded middle. Using the latter is easier. Which one do you have and what does it look like?

11. ## Re: Fitch :(

I see that you don't have the law of excluded middle, but I meant to ask what the negation elimination rule looks like. What formulas does it take and produce? I would guess it takes ~~A and produce A. Is this correct?

Yeah...

13. ## Re: Fitch :(

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.

14. ## Re: Fitch :(

Thank you so much!!!

15. ## Re: Fitch :(

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.