# Thread: Problem with Fitch

1. ## Problem with Fitch

Hi to all, please can anyone help me to understand fitch program. I understand logic part, but not at all how to implement in this program.

Ok, if I have, (p ⇒ ¬q) and (¬q ∧ p ⇒ r) and p, and I have to use the Fitch System to prove r.
p => ~q - Premise
~q & p => r - Premise
p - premise
Goal is r?

And also if I have ((p ⇒ q) ⇒ r), I have to use the Fitch system to prove ((p ⇒ q) ⇒ (p ⇒ r)).

I really appreciate your help.

2. ## Re: Problem with Fitch

Ok, I understand the first one...
Get ~q, then ~q and p to and.Int. to get ~q&P, then ~q&p i ~q&p=>r done Imp.Elm. and get r

Still have problem with other...

3. ## Re: Problem with Fitch

Originally Posted by Alea
Hi to all, please can anyone help me to understand fitch program.
By Fitch program, do you mean some software? I am not familiar with it, but I know Fitch calculus as it is studied in mathematics.

Originally Posted by Alea
p => ~q - Premise
~q & p => r - Premise
p - premise
Goal is r?
From p and p => ~q derive ~q. Then from ~q and p derive ~q & p. From that and ~q & p => r derive r.

Originally Posted by Alea
And also if I have ((p ⇒ q) ⇒ r), I have to use the Fitch system to prove ((p ⇒ q) ⇒ (p ⇒ r)).
To prove ((p ⇒ q) ⇒ (p ⇒ r)), assume p ⇒ q and p. From p ⇒ q and (p ⇒ q) ⇒ r derive r.

4. ## Re: Problem with Fitch

Tnx a loooooooooooooooooooooot!

I have few more problems if you have time and will
_____________________________________________

Given (p ⇒ q) and (r ⇒ s), use the Fitch System to prove (p ∨ r ⇒ q ∨ s).
p => q - premise
r => s - premise

Goal - p | r => q | s

__________________________________________________ ______
Given (¬pq) and (qr), use the Fitch System to prove ((¬p ⇒ ¬r) ⇒ p).
~p => q - premise
q => r - premise

Goal: (~p => ~r) => p

5. ## Re: Problem with Fitch

Originally Posted by Alea
Given (p ⇒ q) and (r ⇒ s), use the Fitch System to prove (p ∨ r ⇒ q ∨ s).
p => q - premise
r => s - premise

Goal - p | r => q | s
Code:
 1. p => q		Assumption
2. r => s		Assumption
3. p | r		Assumption
4.   p			Assumption
5.     q		1, 4: =>E
6.     q | s		5: |I
7.   r			Assumption
8.     s		2, 7: =>E
9.     q | s		8: |I
10.   q | s		3, 4-6, 7-9: |E
11. p | r => q | s	3-10: =>I
Originally Posted by Alea
Given (¬pq) and (qr), use the Fitch System to prove ((¬p ⇒ ¬r) ⇒ p).
~p => q - premise
q => r - premise

Goal: (~p => ~r) => p
This one requires double-negation elimination rule. The most one can derive without it is ~~p from the contraposition of ~p => q.

Assume ~p => ~r and ~p. Derive ~r, q and r by =>E. Then r and ~r give a contradiction, so ~~p. From there double-negation elimination gives p.

Rules dealing with negation may vary from one version of Fitch calculus to another.

6. ## Re: Problem with Fitch

I can get this at all..

10. q | s 3, 4-6, 7-9: |E
11. p | r => q | s 3-10: =>I

Have any clue what I m doing wrong?

7. ## Re: Problem with Fitch

You should apply Or Elimination to p | r. Or Elimination has three components: a disjunction (p | r in this case) and two suberivations. The first derives q | s from an open assumption p, and the second derives the same q | s from an open assumption r. Both subderivations should be at the same nesting level, i.e., same indent. So, after deriving q | s from p, the subderivation should close and a new assumption r should be made at the same indent as p.

I don't understand, by the way, why indent is not increased after the assumption p. E.g., a subderivation that uses the assumption p | r (starting in step 4) is indented compared to p | r, but q in step 5 is not indented compared to p. But maybe I don't know the details of the program.