 Solution

ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2017/digital-systems-linear-algebra-introduction-to-formal-proof/7/a/v/solution

Apply the biconditional introduction rule from part (iv) to the two already established derivations:

\frac{\neg ( P \to \neg Q ) ⊢ Q \land P Q \land P ⊢ \neg ( P \to \neg Q )}{⊢ \neg ( P \to \neg Q ) \leftrightarrow ( Q \land P )} .

The left numerator is part (iii), the right is part (i). Introduction discharges both displayed assumptions, so the result has no premises.

 New to topics? Read the docs here!