Solution

ID: past-exam-of-the-logic-and-set-theory-course-of-the-university-of-oxford/2010/a/2/b/solution

Write and . All derivations below use the printed replacement axiom, so they do not rely on the false equivalence from part (a).
The identity logical implication follows by the deduction rule. Substituting , into the replacement axiom and applying modus ponens rule therefore gives double-negation elimination:
Universal instantiation gives . Combine it with using modus ponens rule under a temporary assumption and then the deduction rule, obtaining .
In the replacement axiom now substitute and . Its antecedent is precisely the last theorem, and its consequent is . Thus
Under the fixed assumption and temporary assumption , modus ponens rule gives and then . Discharge the temporary assumption to obtain .
Finally apply universal generalization. The variable is not free in , because it is bound in and is not free in by hypothesis. Hence the side condition is satisfied and
Generalization is applied after the temporary assumption has been discharged; applying it while that assumption remained open would not be justified.

New to topics? Read the docs here!