Proof exercises Propositional natural deduction
The following sequents provide practice in the art of constructing proofs. Answers are given, but of course the idea is to come up with proofs of your own before looking them up. As ever, the answers are not unique: in some cases, alternative proofs are just as good as the ones given.
| (p AND q) AND r ⊢ s OR (q OR t) | SH {Sample proof 1} SP {(p AND q) AND r ⊢ s OR (q OR t)} PL {1} {1} {(p AND q) AND r} {A} PL {1} {2} {p AND q)} {1 ANDE} PL {1} {3} {q} {2 ANDE} PL {1} {4} {q OR t} {3 ORI} PL {1} {5} {s OR (q OR t)} {4 ORI} EP EH | Try it | Answer | |
| (p IMP q) IMP p ⊢ (p IMP q) IMP q | SH {Sample proof 2} 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} {4} {q} {2, 3 IMPE} PL {1} {5} {p IMP q) IMP q} {4 [2] IMPI} EP EH | Try it | Answer | |
| (p AND q) IMP NOTr ⊢ (p AND r) IMP NOTq | SH {Sample proof 3} SP {(p AND q) IMP NOTr ⊢ (p AND r) IMP NOTq} PL {1} {1} {(p AND q) IMP NOTr} {A} PL {2} {2} {p AND r} {A} PL {3} {3} {q} {A} PL {2} {4} {p} {2 ANDE} PL {2,3} {5} {p AND q} {3, 4 ANDI} PL {1,2,3} {6} {NOTr} {1, 5 IMPE} PL {2} {7} {r} {2 ANDE} PL {1,2} {8} {NOTq} {6, 7 [3] RAA} PL {1} {9} {(p AND r) IMP NOTq} {8 [2] IMPI} EP EH | Try it | Answer | |
| p IMP q ⊢ (q IMP r) IMP ((r IMP s) IMP (NOTs IMP NOTp)) | SH {Sample proof 4} SP {p IMP q ⊢ (q IMP r) IMP ((r IMP s) IMP (NOTs IMP NOTp))} PL {1} {1} {p IMP q} {A} PL {2} {2} {q IMP r} {A} PL {3} {3} {r IMP s} {A} PL {4} {4} {NOTs} {A} PL {5} {5} {p} {A} PL {1,5} {6} {q} {1, 5 IMPE} PL {1,2,5} {7} {r} {2, 6 IMPE} PL {1,2,3,5} {8} {s} {3, 7 IMPE} PL {1,2,3,4} {9} {NOTp} {4, 8 [5] RAA} PL {1,2,3} {10} {NOTs IMP NOTp} {9 [4] IMPI} PL {1,2} {11} {(r IMP s) IMP (NOTs IMP NOTp)} {10 [3] IMPI} PL {1} {12} {(q IMP r) IMP ((r IMP s) IMP (NOTs IMP NOTp))} {11 [2] IMPI} EP EH | Try it | Answer | |
| p AND q ⊢ (p IMP q) AND (q IMP p) | SH {Sample proof 5} SP {p AND q ⊢ (p IMP q) AND (q IMP p)} PL {1} {1} {p AND q} {A} PL {1} {2} {p} {1 ANDE} PL {1} {3} {q} {1 ANDE} PL {1} {4} {p IMP q} {3 [ ] IMPI} PL {1} {5} {q IMP p} {2 [ ] IMPI} PL {1} {6} {(p IMP q) AND (q IMP p)} {4, 5 ANDI} EP EH | Try it | Answer | |
| NOT(NOTp AND NOTq) ⊢ p OR q | SH {Sample proof 6} SP {NOT(NOTp AND NOTq) ⊢ p OR q} PL {1} {1} {NOT(NOTp AND NOTq)} {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 {6} {6} {q} {A} PL {6} {7} {p OR q} {6 ORI} PL {2} {8} {NOTq} {2, 7 [6] RAA} PL {2} {9} {NOTp AND NOTq} {5, 8 ANDI} PL {1} {10} {¬NOT(p OR q)} {1, 9 [2] RAA} PL {1} {11} {p OR q} {10 NOTNOTE} EP EH | Try it | Answer | |
| p IMP NOTq ⊢ (p AND q) IMP r | SH {Sample proof 7} SP {p IMP NOTq ⊢ (p AND q) IMP r} PL {1} {1} {p IMP NOTq} {A} PL {2} {2} {p AND q} {A} PL {2} {3} {p} {2 ANDE} PL {2} {4} {q} {2 ANDE} PL {1,2} {5} {NOTq} {1, 3 IMPE} PL {1,2} {6} {NOTNOTr} {4, 5 [ ] RAA} PL {1,2} {7} {r} {6 NOTNOTE} PL {1} {8} {(p AND q) IMP r} {7 [2] IMPI} EP EH | Try it | Answer | |
| p OR q ⊢ NOTp IMP q | SH {Sample proof 8} 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 {1,2} {7} {q} {1, 5 [3], 6 [6] ORE} PL {1} {8} {NOTp IMP q} {7 [2] IMPI} EP EH | Try it | Answer | |
| NOTp IMP q ⊢ p OR q | SH {Sample proof 9} 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 | |
| NOT(p IMP q) ⊢ p AND NOTq | SH {Sample proof 10} SP {NOT(p IMP q) ⊢ p AND NOTq} PL {1} {1} {NOT(p IMP 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 {2} {6} {p IMP q} {5 [3] IMPI} PL {1} {7} {NOTNOTp} {1, 6 [2] RAA} PL {1} {8} {p} {7 NOTNOTE} PL {9} {9} {q} {A} PL {9} {10} {p IMP q} {9 [ ] IMPI} PL {1} {11} {NOTq} {1, 10 [9] RAA} PL {1} {12} {p AND NOTq} {8, 11 ANDI} EP EH | Try it | Answer | |
| (p IMP q) IMP q ⊢ (q IMP p) IMP p | SH {Sample proof 11} SP {(p IMP q) IMP q ⊢ ((q IMP p) IMP p} PL {1} {1} {(p IMP q) IMP q} {A} PL {2} {2} {q IMP p} {A} PL {3} {3} {NOTp} {A} PL {4} {4} {p} {A} PL {3,4} {5} {NOTNOTq} {3, 4 [ ] RAA} PL {3,4} {6} {q} {5 NOTNOTE} PL {3} {7} {p IMP q} {6 [4] IMPI} PL {1,3} {8} {q} {1, 7 IMPE} PL {1,2,3} {9} {p} {2, 8 IMPE} PL {1,2} {10} {NOTNOTp} {3, 9 [3] RAA} PL {1,2} {11} {p} {10 NOTNOTE} PL {1} {12} {(q IMP p) IMP p} {11 [2] IMPI} EP EH | Try it | Answer | |
| p IMP q, r IMP s ⊢ (p OR r) IMP (q OR s) | SH {Sample proof 12} 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 {7} {7} {r} {A} PL {2,7} {8} {s} {2, 7 IMPE} PL {2,7} {9} {q OR s} {8 ORI} PL {1,2,3} {10} {q OR s} {3, 6 [4], 9 [7] ORE} PL {1,2} {11} {(p OR r) IMP (q OR s)} {10 [3] IMPI} EP EH | Try it | Answer | |
| p OR q, p OR r, NOT(q AND r) ⊢ p | SH {Sample proof 13} SP {p OR q, p OR r, NOT(q AND r) ⊢ p} PL {1} {1} {p OR q} {A} PL {2} {2} {p OR r} {A} PL {3} {3} {NOT(q AND r)} {A} PL {4} {4} {p} {A} PL {5} {5} {q} {A} PL {6} {6} {r} {A} PL {5,6} {7} {q AND r} {5, 6 ANDI} PL {3,5,6} {8} {NOTNOT p} {3, 7 [ ] RAA} PL {3.5.6} {9} {p} {8 NOTNOTE} PL {2,3,5} {10} {p} {2, 4 [4], 9 [6] ORE} PL {1,2,3} {11} {p} {1, 4 [4], 10 [5] ORE} EP EH | Try it | Answer | |
| p IMP (q OR r) ⊢ NOTq IMP (p IMP r) | SH {Sample proof 14} SP {p IMP (q OR r) ⊢ NOTq IMP (p IMP r)} PL {1} {1} {p IMP (q OR r)} {A} PL {2} {2} {NOTq} {A} PL {3} {3} {p} {A} PL {1,3} {4} {q OR r} {1, 3 IMPE} PL {5} {5} {q} {A} PL {2,5} {6} {NOTNOTr} {2, 5 [ ] RAA} PL {2,5} {7} {r} {6 NOT¬E} PL {8} {8} {r} {A} PL {1,2,3} {9} {r} {4, 7 [5], 8 [8] ORE} PL {1,2} {10} {p IMP r} {9 [3] IMPI} PL {1} {11} {NOTq IMP (p IMP r)} {10 [2] IMPI} EP EH | Try it | Answer | |
| (p AND q) IMP (r OR s) ⊢ (p IMP r) OR (q IMP s) | SH {Sample proof 15} SP {(p AND q) IMP (r OR s) ⊢ (p IMP r) OR (q IMP s)} PL {1} {1} {(p AND q) IMP (r OR s)} {A} PL {2} {2} {NOT((p IMP r) OR (q IMP s))} {A} PL {3} {3} {p} {A} PL {4} {4} {q} {A} PL {3,4} {5} {p AND q} {3, 4 ANDI} PL {1,3,4} {6} {r OR s} {1, 5 IMPE} PL {7} {7} {r} {A} PL {7} {8} {p IMP r} {7 [ ] IMPI} PL {7} {9} {(p IMP r) OR (q IMP s)} {8 ORI} PL {10} {10} {s} {A} PL {10} {11} {q IMP s} {10 [ ] IMPI} PL {10} {12} {(p IMP r) OR (q IMP s)} {11 ORI} PL {1,3,4} {13} {(p IMP r) OR (q IMP s)} {6, 9 [7], 12 [10] ORE} PL {1,2,3,4} {14} {NOTNOTs} {2, 13 [ ] RAA} PL {1,2,3,4} {15} {s} {14 NOTNOTE} PL {1,2,3} {16} {q IMP s} {15 [4] IMPI} PL {1,2,3} {17} {(p IMP r) OR (q IMP s)} {16 ORI} PL {1,2,3} {18} {NOTNOTr} {2, 17 [ ] RAA} PL {1,2,3} {19} {r} {18 NOTNOTE} PL {1,2} {20} {p IMP r} {19 [3] IMPI} PL {1,2} {21} {(p IMP r) OR (q IMP s)} {20 ORI} PL {1} {22} {NOTNOT((p IMP r) OR (q IMP s))} {2, 21 [2] RAA} PL {1} {23} {(p IMP r) OR (q IMP s)} {22 NOTNOTE} EP EH | Try it | Answer |