THE LOGIC NOTES

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) Try it Answer
(p IMP q) IMP p   ⊢   (p IMP q) IMP q Try it Answer
(p AND q) IMP NOTr   ⊢   (p AND r) IMP NOTq Try it Answer
p IMP q   ⊢   (q IMP r) IMP ((r IMP s) IMP (NOTs IMP NOTp)) Try it Answer
p AND q   ⊢   (p IMP q) AND (q IMP p) Try it Answer
NOT(NOTp AND NOTq)   ⊢   p OR q Try it Answer
p IMP NOTq   ⊢   (p AND q) IMP r Try it Answer
p OR q   ⊢   NOTp IMP q Try it Answer
NOTp IMP q   ⊢   p OR q Try it Answer
NOT(p IMP q)   ⊢   p AND NOTq Try it Answer
(p IMP q) IMP q   ⊢   (q IMP p) IMP p Try it Answer
p IMP q, r IMP s   ⊢   (p OR r) IMP (q OR s) Try it Answer
p OR q, p OR r, NOT(q AND r)   ⊢   p Try it Answer
p IMP (q OR r)   ⊢   NOTq IMP (p IMP r) Try it Answer
(p AND q) IMP (r OR s)   ⊢   (p IMP r) OR (q IMP s) Try it Answer