Proof 3 sequents with natural deduction

53 Views Asked by At

I have to proof 3 sequents and allowed are the basic rules like elimination, implication, pbc and so on. I am kinda struggling with the solutions but maybe you can give me some hints. :)

1) -p -> p |- p

1.| -p -> p (premise)
2.|| -p (Assumption)
3.|| p (Implication elimination 1,2)
4.|| false (Negation elimination 2,3)
5.| p (Proof by contradiction 2-4)

Have I proofed it correctly?

2) p v q, -r -> -p |- q v r

1.| p v q (premise)
2.| -r -> -p (premise)
3.|| p (assumption)
4.|| --r (MT 2,3)
5.|| r (--e 4)
6.|| q v r (v i2 5)
7.|| q (Assumption)
8.|| q v r ( v i1 7)
9.| q v r (v E 1, 3-6, 7-8)

Update: This is my proof for sequent 2 now. Can I derive q like this?

3) -(p -> q) |- q -> p

1.| -(p -> q) (premise)
2.|| q (assumption)
3.||| p (assumption)
4.||| p -> q (-> i 2-3)
5.||| false (-e 1,4)
6.|| -p (-i 3-5)
7.|| false (-e 3-6)
8.|| p (false e 7)
9.| q -> p (-> i 2-8)

Update: Here is my mew version.

1

There are 1 best solutions below

2
On BEST ANSWER
1.| -(p -> q) (premise)
2.|| q (assumption)
3.||| p (assumption)
4.||| p -> q (-> i 2-3)   Error: -> introduction discharges the assumption
5.||| false (-e 1,4)
6.|| -p (-i 3-5)          
7.|| false (-e 3-6)       Error: line 3 is inaccessible
8.|| p (false e 7)
9.| q -> p (-> i 2-8) 

Still, you have the right idea. With a slignt ammendment:

1.| -(p -> q)   (premise)
2.| | q          (assumption)
3.| | | p         (assumption)
4.| | | q         (reiteration)
5.| | p -> q     (-> i, 3-4)
6.| | #          (- e, 1,5)
7.| | p          (explosion, 6)
8.| q -> p      (-> i 2-7)