Non-classical proof exercises Challenging the Paradigm
The following sequents are to be proved in the logics R or F*, or in some cases in their common core. Comparison with the earlier propositional logic exercises may be useful. The proof editor can handle these logics, but you will need to take note of its ways of handlling the structural rules, which are not exactly the raw versions given in the notes. It does not distinguish between contraction and importation, since these are essentially equivalent, and similarly it does not distinguish between exportation and weakening. It also allows vacuous discharge in the case of F*, though not of course in the case of R. Anyway, to deepen your understanding of logic and proof, these exercises are recommended. Please enjoy them!
| [R and F*] | p AND (q OR r) ⊢ (p AND q) OR r | SH {Sample proof 501 (in R and F*)} SP {p AND (q OR r) ⊢ (p AND q) OR r} PL {1} {1} {p AND (q OR r)} {A} PL {1} {2} {p} {1 ANDE} PL {1} {3} {q OR r} {1 ANDE} PL {4} {4} {q} {A} PL {1,4} {5} {p AND q} {2, 4 ANDI} PL {1,4} {6} {(p AND q) OR r} {5 ORI} PL {7} {7} {r} {A} PL {7} {8} {(p AND q) OR r} {7 ORI} PL {1,7} {9} {(p AND q) OR r} {8 eK} PL {1} {10} {(p AND q) OR r} {3, 6 [4], 9 [7] ORE} EP EH | Try it | Answer | |
| [R] | (p IMP q) IMP p ⊢ (p IMP q) IMP q | SH {Sample proof 502 (in R)} SP {(p IMP q) IMP p ⊢ (p IMP q) IMP q} PL {1} {1} {(p IMP q) IMP p} {A} PL {2} {2} {p IMP q} {A} PL {1;2} {3} {p} {1, 2 IMPE} PL {1;2;2} {4} {q} {2, 3 IMPE} PL {1;2} {5} {q} {4 contraction} PL {1} {6} {p IMP q) IMP q} {5 [2] IMPI} EP EH | Try it | Answer | |
| [R and F*] | p IMP (q IMP NOTr) ⊢ q IMP (r IMP NOTp | SH {Sample proof 503 (in R and F*)} SP {p IMP (q IMP NOTr) ⊢ q IMP (r IMP NOTp)} PL {1} {1} {p IMP (q IMP NOTr)} {A} PL {2} {2} {q} {A} PL {3} {3} {r} {A} PL {4} {4} {p} {A} PL {1;4} {5} {q IMP NOTr} {1, 4 IMPE} PL {1;2;4} {6} {NOTr} {2, 5 IMPE} PL {1;2;3} {7} {NOTp} {3, 6 [4] RAA} PL {1;2} {8} {r IMP NOTp} {7 [4] IMPE} PL {1} {9} {q IMP (r IMP NOTp)} {8 [2] IMPI} EP EH | Try it | Answer | |
| [F*] | p IMP (q IMP p) ⊢ q IMP (p IMP (q IMP p)) | SH {Sample proof 504 (in F*)} SP {p IMP (q IMP p) ⊢ q IMP (p IMP (q IMP p))} PL {1} {1} {p IMP (q IMP p)} {A} PL {1} {2} {q IMP (p IMP (q IMP p))} {1 [ ] IMPI} EP EH | Try it | Answer | |
| [R] | p IMP (q IMP p) ⊢ q IMP (p IMP (q IMP p)) | SH {Sample proof 505 (in R)} SP {p IMP (q IMP p) ⊢ q IMP (p IMP (q IMP p))} PL {1} {1} {p IMP (q IMP p)} {A} PL {2} {2} {q} {A} PL {3} {3} {p} {A} PL {1;3} {4} {q IMP p} {1, 3 IMPE} PL {1;2;3} {5} {p} {2, 4 IMPE} PL {1;1;2;3} {6} {q IMP p} {1, 5 IMPE} PL {1;1;2;2;3} {7} {p} {2, 6 IMPE} PL {1;2;2;3} {8} {p} {7 contraction} PL {1;2;3} {9} {q IMP p} {8 [2] IMPI} PL {1;2} {10} {p IMP (q IMP p)} {9 [3] IMPI} PL {1} {11} {q IMP (p IMP (q IMP p))} {10 [2] IMPI} EP EH | Try it | Answer | |
| [R] | p, NOTq ⊢ NOT(p IMP q) | SH {Sample proof 506 (in R)} SP {p, NOTq ⊢ NOT(p IMP q)} PL {1} {1} {p} {A} PL {2} {2} {NOT q} {A} PL {3} {3} {p IMP q} {A} PL {1;3} {4} {q} {1, 3 IMPE} PL {1;2} {5} {NOT(p IMP q)} {2, 4 [3] RAA} PL {1,2} {6} {NOT(p IMP q)} {5 contraction} EP EH | Try it | Answer | |
| [F*] | NOT(p IMP q) ⊢ p AND NOTq | SH {Sample proof 507 (in F*)} SP {NOT(p IMP q) ⊢ p AND NOTq} PL {1} {1} {NOT(p IMP q)} {A} PL {2} {2} {q} {A} PL {2} {3} {p IMP q} {2 [ ] IMPI} PL {1} {4} {NOTq} {1, 3 [2] RAA} PL {5} {5} {NOTp} {A} PL {6} {6} {p} {A} PL {5,6} {7} {NOTNOTq} {5, 6 [ ] RAA} PL {5,6} {8} {q} {7 NOTNOTE} PL {5} {9} {p IMP q} {8 [6] IMPI} PL {1} {10} {NOTNOTp} {1, 9 [3] RAA} PL {1} {11} {p} {10 NOTNOTE} PL {1} {12} {p AND NOTq} {4, 11 ANDI} EP EH | Try it | Answer | |
| [F*] | p OR q ⊢ NOTp IMP q | SH {Sample proof 508 (in F*)} SP {p OR q ⊢ NOTp IMP q} PL {1} {1} {p OR q} {A} PL {2} {2} {NOTp} {A} PL {3} {3} {p} {A} PL {2;3} {4} {NOTNOTq} {2, 3 [ ] RAA} PL {2;3} {5} {q} {4 NOTNOTE} PL {6} {6} {q} {A} PL {2;6} {7} {q} {6, weakening} PL {1;2} {7} {q} {1, 5 [3], 7 [6] ORE} PL {1} {8} {NOTp IMP q} {7 [2] IMPI} EP EH | Try it | Answer | |
| [R] | NOTp IMP q ⊢ p OR q | SH {Sample proof 509 (in R)} SP {NOTp IMP q ⊢ p OR q} PL {1} {1} {NOTp IMP q} {A} PL {2} {2} {NOT(p OR q)} {A} PL {3} {3} {p} {A} PL {3} {4} {p OR q} {3 ORI} PL {2} {5} {NOTp} {2, 4 [3] RAA} PL {1;2} {6} {q} {1, 5 IMPE} PL {1;2} {7} {p OR q} {6 ORI} PL {1} {8} {NOTNOT(p OR q)} {2, 7 [2] RAA} PL {1} {9} {p OR q} {8 NOTNOTE} EP EH | Try it | Answer | |
| [F*] | p IMP q ⊢ (p AND r) IMP (q AND r) | SH {Sample proof 510 (in F*)} SP {p IMP q ⊢ (p AND r) IMP (q AND r)} PL {1} {1} {p IMP q} {A} PL {2} {2} {p AND r} {A} PL {2} {3} {p} {2 ANDE} PL {1;2} {4} {q} {1, 3 IMPE} PL {2} {5} {r} {2 ANDE} PL {1;2} {6} {r} {5 weakening} PL {1;2} {7} {q AND r} {4, 6 ANDI} PL {1} {8} {(p AND r) IMP (q AND r)} {7 [2] IMPI} EP EH | Try it | Answer | |
| [R] | p IMP q ⊢ (NOTp IMP p) IMP (NOTq IMP q) | SH {Sample proof 511 (in R)} SP {p IMP q ⊢ (NOTp IMP p) IMP (NOTq IMP q)} PL {1} {1} {p IMP q} {A} PL {2} {2} {NOTp IMP p} {A} PL {3} {3} {NOTq} {A} PL {4} {4} {p} {A} PL {1;4} {5} {q} {1, 4 ANDE} PL {1;3} {6} {NOTp} {3, 5 [4] RAA} PL {1;2;3} {7} {p} {2, 6 IMPE} PL {1;1;2;3} {8} {q} {1, 7 IMPE} PL {1;2;3} {9} {q} {8 contraction} PL {1;2} {10} {NOTq IMP q} {9 [3] IMPI} PL {1} {11} {(NOTp IMP p) IMP (NOTq IMP q)} {10 [2] IMPI} EP EH | Try it | Answer | |
| [R and F*] | p IMP q, r IMP s ⊢ (p OR r) IMP (q OR s) | SH {Sample proof 512 (in R and F*)} SP {p IMP q, r IMP s ⊢ (p OR r) IMP (q OR s)} PL {1} {1} {p IMP q} {A} PL {2} {2} {r IMP s} {A} PL {3} {3} {p OR r} {A} PL {4} {4} {p} {A} PL {1;4} {5} {q} {1, 4 IMPE} PL {1;4} {6} {q OR s} {5 ORI} PL {(1,2);4} {7} {q OR s} {6 eK} PL {8} {8} {r} {A} PL {2;8} {9} {s} {2, 8 IMPE} PL {2;8} {10} {q OR s} {9 ORI} PL {(1,2);8} {11} {q OR s} {10 eK} PL {(1,2);3} {12} {q OR s} {3, 7 [4], 11 [8] ORE} PL {1,2} {13} {(p OR r) IMP (q OR s)} {12 [3] IMPI} EP EH | Try it | Answer | |
| [F*] | p IMP (q OR r); (p AND q) IMP r ⊢ p IMP r | SH {Sample proof 513 (in F*)} SP {p IMP (q OR r); (p AND q) IMP r ⊢ p IMP r} PL {1} {1} {p IMP (q OR r)} {A} PL {2} {2} {(p AND q) IMP r} {A} PL {3} {3} {p} {A} PL {1;3} {4} {q OR r} {1, 3 IMPE} PL {5} {5} {q} {A} PL {3,5} {6} {p AND q} {3, 5 ANDI} PL {2;(3,5)} {7} {r} {2, 6 IMPE} PL {8} {8} {r} {A} PL {2;(3,8)} {9} {r} {8 weakening} PL {((1;3),3);2} {10} {r} {4, 7 [5], 9 [8] ORE} PL {1;2;3} {11} {r} {10 weakening} PL {1;2} {12} {p IMP r} {11 [3] IMPI} EP EH | Try it | Answer |