Past exam of the logic and set theory course of the University of Oxford / 2010 / A / 2 / b

Write $U=\forall x_i\neg \varphi$ and $H=\neg U\to \psi$. All derivations below use the printed replacement axiom, so they do not rely on the false equivalence from part (a).

The identity logical implication $\neg A\to \neg A$ follows by the deduction rule. Substituting $\alpha =\neg A$, $\beta =A$ into the replacement axiom and applying modus ponens rule therefore gives double-negation elimination:Universal instantiation gives $⊢U\to \neg \varphi$. Combine it with $⊢\neg \neg U\to U$ using modus ponens rule under a temporary assumption and then the deduction rule, obtaining $⊢\neg \neg U\to \neg \varphi$.

In the replacement axiom now substitute $\alpha =\neg \varphi$ and $\beta =\neg U$. Its antecedent is precisely the last theorem, and its consequent is $\neg \neg \varphi \to \neg U$. ThusUnder the fixed assumption $H$ and temporary assumption $\neg \neg \varphi$, modus ponens rule gives $\neg U$ and then $\psi$. Discharge the temporary assumption to obtain $H⊢\neg \neg \varphi \to \psi$.

Finally apply universal generalization. The variable $x_i$ is not free in $H$, because it is bound in $U$ and is not free in $\psi$ by hypothesis. Hence the side condition is satisfied andGeneralization is applied after the temporary assumption has been discharged; applying it while that assumption remained open would not be justified.