Final version: Feb 24
Resources: chapter 4 (“New proofs from old”) of How Logic Works.
For the following four problems, you may cut in any of the “useful validities” from pp 233-4 in the textbook (cite them by name or number), or any other sequent for which you include a proof. Please note that ↔︎ intro and elim are defined on page 59 of the textbook.
Prove that ¬(P↔︎Q) ⊢ P → ¬Q. Hint: you can use the following valid sequent: A, B ⊢ A ↔︎ B (biconditional).
Prove that P ↔︎ Q, ¬(P∧Q) ⊢ ¬P ∧ ¬Q.
Prove that P ↔︎ Q ⊢ (P∧Q) ∨ (¬P∧¬Q). Hint: use sequents that you already proved in this pset and/or the sequent ¬A → B ⊢ A ∨ B (material conditional).
Prove that ⊢ (P↔︎Q) ∨ (P↔︎¬Q).
Explain (in a half page or less) how you know that there is a correctly written proof whose final line has the formula (P↔︎Q) ∨ ((Q↔︎R)∨(P↔︎R)) and no dependency numbers. A good answer will cite the completeness of our rules of inference.
Please argue for or against the claim that the following proof rule can be derived from those we already have. You answer should be maximum a half page, and a good answer will likely say something about the relationship between proofs and truth tables.
From Γ ⊢ ¬(P∧Q) it is permitted to derive Γ ⊢ ¬P. In other words, if you have ¬(P∧Q) on a line with dependencies Γ, then you may write ¬P on a subsequent line, also with dependencies Γ.