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.
Still, you have the right idea. With a slignt ammendment: