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...
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.
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 (¬p ⇒ q) and (q ⇒ r), use the Fitch System to prove ((¬p ⇒ ¬r) ⇒ p).
~p => q - premise
q => r - premise
Goal: (~p => ~r) => p
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
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.
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.