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

Let $f=\alpha \to (\beta \to \gamma )$ and $h=\alpha \to \beta$. Temporarily assume $f$, $h$, and $\alpha$. Modus ponens rule first gives $\beta \to \gamma$ from $f$ and $\alpha$, then $\beta$ from $h$ and $\alpha$, and finally $\gamma$.

Apply the deduction theorem for propositional logic successively to discharge $\alpha$, then $h$, then $f$. The result isthe required axiom scheme. This derivation uses only assumptions, modus ponens rule, and the added deduction rule; no negation axiom is involved.

The requested derivation does not follow from the printed axiom set. Use a two-valued matrix interpretation with ordinary material logical implication and designated value $1$, but interpret the unary symbol $\neg$ by the constant function $N(0)=N(1)=0$.

Every instance of the first axiom $\alpha \to (\beta \to \alpha )$ is valid. In the replacement axiom, both $N(\beta )\to \alpha$ and $N(\alpha )\to \beta$ have value $1$, so its whole logical implication is valid as well. Modus ponens rule preserves the designated value. The deduction rule is sound for semantic consequence under this interpretation because logical implication is the ordinary truth-functional logical implication. Induction on derivations, allowing arbitrary sets of assumptions, therefore makes every theorem valid in this matrix.

But the old contraposition axiom has valuewhich is false when $\alpha =1$ and $\beta =0$. ConsequentlyThis is a truth-matrix countermodel for a Hilbert axiom set. A nonstandard interpretation of a primitive symbol is legitimate for proving syntactic nonderivability: only preservation by the displayed axioms and rules is required. The source would need a stronger negation axiom or an extra negation principle to support its requested conclusion.

The old system does derive the replacement axiom. Here is a syntactic proof using only its axioms, modus ponens rule, and the permitted deduction theorem for propositional logic.

First derive explosion. From $U$ and $\neg U$, the first axiom gives $\neg V\to \neg U$. The old third axiom then gives $U\to V$, and modus ponens rule with $U$ gives any desired $V$.

Next derive the classical reductio rule. Suppose $\Gamma ,\neg B$ derives both $C$ and $\neg C$. Let $T$ be the theorem $B\to B$, obtainable by applying the deduction theorem for propositional logic to the identity derivation from assumption $B$. Explosion under $\Gamma ,\neg B$ gives $\neg T$, so the deduction theorem for propositional logic gives $\Gamma ⊢\neg B\to \neg T$. The old third axiom with $\alpha =T$, $\beta =B$ yields $\Gamma ⊢T\to B$. Since $T$ is a theorem, $\Gamma ⊢B$. Thus a contradiction under $\neg B$ permits deriving $B$ with that temporary assumption discharged.

Now assume $h=\neg \beta \to \alpha$ and $\neg \alpha$, and temporarily also assume $\neg \beta$. Modus ponens rule gives $\alpha$, contradicting $\neg \alpha$. The just-proved reductio rule discharges $\neg \beta$ and gives $\beta$. Finally discharge $\neg \alpha$ and $h$ by the deduction theorem for propositional logic:No propositional completeness theorem is needed in this derivation.

Only one logical implication of the printed equivalence is justified:The new system's first axiom is an old axiom, its replacement axiom is derivable in the old system by part (iii), modus ponens rule is shared, and its deduction rule is admissible in the old system by the theorem allowed in the source. Induction on a new-system derivation therefore translates it into an old-system derivation with the same assumptions.

The reverse logical implication is false for the displayed systems. Take $\Gamma =\varnothing$ and let $\varphi$ be an instance of the old contraposition axiom, for example with distinct propositional variables in place of $\alpha ,\beta$. It is an old-system theorem, but the matrix countermodel in part (ii) refutes its derivability in the new system. Thus the requested two-way equivalence cannot be concluded from these printed axioms.

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.