0

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.

canon
  • 31
  • For 2), your concern is correct : you have derived $q \lor r$ under assumption $p$. In order to complete the proof, you have to derive it also under assumption $q$, and then apply $\lor$-elim, – Mauro ALLEGRANZA Oct 17 '18 at 18:27
  • For 3) after $q$ you have not to assume $p \to q$ but derive it from $q$. Thus you have a contradiction and you can derive $p$ and then $p \to q$ by $\to$-intro, – Mauro ALLEGRANZA Oct 17 '18 at 18:29
  • A similar problem, which could be used as an intermediate step in (3): $\lnot(p \rightarrow q) \vdash p$. In fact, $\lnot(p \rightarrow q) \vdash p \wedge \lnot q$. – Daniel Schepler Oct 17 '18 at 18:56
  • @MauroALLEGRANZA: Hey thx for the clues. I have updated number 2. I think it is correct now. To 3: How should I derive p -> q from q? – canon Oct 17 '18 at 19:05
  • Yes, now 2 is correct. – Mauro ALLEGRANZA Oct 17 '18 at 19:25
  • Basically, assume $p$, then $q$, then derive $p \to q$ by $\to$-intro, discharging $p$. – Mauro ALLEGRANZA Oct 17 '18 at 19:26
  • @MauroALLEGRANZA I have updated number 3. I wasn't sure if I can introduce in step 4 an introduction like this. If not I can add 2 extra lines to change the order of the assumptions. – canon Oct 17 '18 at 20:49

1 Answers1

0
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)
Graham Kemp
  • 129,094