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

A logical derivation from $\Gamma$ is a finite sequence of propositional formulas, each either a member of $\Gamma$, an instance of one of the three axioms, or obtained from earlier lines by one of the two displayed inference rules. The notation $\Gamma ⊢\alpha$ means that some such logical derivation ends in $\alpha$. Writing $⊢\alpha$ means derivability with no assumptions.

Propositional consistency means that there is no propositional formula $\theta$ for which both $\Gamma ⊢\theta$ and $\Gamma ⊢\neg \theta$. Equivalently not every propositional formula is derivable. To check the equivalence directly for this calculus, use the identity theorem proved in (ii): from $\theta \to \theta$ and L3 obtain $\theta \to (\neg \theta \to \eta )$; two uses of modus ponens rule give arbitrary $\eta$. Thus a contradictory theory proves everything. Conversely a theory proving everything proves a propositional formula and its negation.

Choose an auxiliary propositional formula $\beta$. The two instances of L1 areThe instance of L2 with $\gamma =\alpha$ isApply modus ponens rule first with the first L1 instance and then with the second. This is an assumption-free logical derivation, soIn particular no semantic completeness theorem or deduction theorem for propositional logic has been assumed to obtain this identity theorem.

An instance of L3 isUsing the first assumed logical derivation and modus ponens rule gives $\Gamma ⊢\alpha \to (\neg \beta \to \gamma )$. The L2 instance for these same three propositional formulas isUse the other assumed logical derivation and then the newly obtained logical derivation in two applications of modus ponens rule. ThereforeThis conditional modus ponens construction is the step needed to discharge assumptions from a modus ponens rule line in part (iv).

For this calculus the deduction theorem for propositional logic isFor the reverse logical implication, retain the logical derivation from $\Gamma$, add the assumption $\alpha$, and use modus ponens rule.

For the forward logical implication, induct on a logical derivation from $\Gamma \cup \{\alpha \}$. For each line $\delta$ we construct a logical derivation of $\alpha \to \delta$ from $\Gamma$. If $\delta =\alpha$, use (ii). If $\delta$ is an axiom instance or belongs to $\Gamma$, it is already derivable from $\Gamma$; L1 gives $\delta \to (\alpha \to \delta )$, and modus ponens rule finishes that case.

If $\delta$ comes from $\eta$ and $\eta \to \delta$ by modus ponens rule, the induction hypothesis suppliesPart (iii) supplies $\Gamma ⊢\alpha \to \delta$.

If $\delta$ comes by the elimination rule E from $\eta \to \delta$ and $\neg \eta \to \delta$, the induction hypothesis suppliesThe L2 instance with $(\alpha ,\beta ,\gamma )=(\alpha ,\eta ,\delta )$ combines these by two applications of modus ponens rule. Thus the rule E also survives the discharge construction. These are all possible lines, proving the theorem for the final line $\beta$.

Suppose both extensions were inconsistent. By the explosion argument in (i), the extension by $\varphi$ proves $\neg \varphi$, and the extension by $\neg \varphi$ proves $\varphi$. The deduction theorem for propositional logic therefore yieldsThe identity theorem gives $⊢\neg \varphi \to \neg \varphi$ and $⊢\varphi \to \varphi$. Apply E to the first displayed logical implication and the identity logical implication with antecedent $\neg \varphi$ to obtain $\Gamma ⊢\neg \varphi$. Apply E to the identity logical implication with antecedent $\varphi$ and the second displayed logical implication to obtain $\Gamma ⊢\varphi$. This contradicts propositional consistency of $\Gamma$.

Consequently at least one of the two one-formula extensions is propositionally consistent. The formal proof uses the source's own calculus, including its rule E, rather than assuming an unproved completeness theorem for this presentation.