Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Digital systems, linear algebra, introduction to formal proof / 7

The conjunction introduction rule derives $\varphi \wedge \psi$ from proofs of $\varphi$ and $\psi$ in the current context. The disjunction elimination rule derives a common conclusion $\kappa$ from $\varphi \vee \psi$, a subproof of $\kappa$ under temporary assumption $\varphi$, and a subproof of $\kappa$ under temporary assumption $\psi$. The implication introduction rule derives $\varphi \to \psi$ by temporarily assuming $\varphi$ and proving $\psi$.

The rectangular boxes delimit subproofs and the scope of their temporary assumptions. The disjunction elimination rule discharges the two case assumptions; the implication introduction rule discharges its antecedent assumption. Formulas depending on a boxed assumption cannot simply escape that box. Other undischarged assumptions remain in force, and nested boxes can access the assumptions of enclosing boxes.

Work backwards from the outermost available logical connective. One strategy applies the disjunction elimination rule to the premise first, constructs the whole target in each case, and then closes the cases. In the tables, a context such as $\{1,2\}$ means that assumptions on lines 1 and 2 remain open. A range in a discharge rule denotes the entire local subproof.

A second strategy applies the conjunction introduction rule backwards to the target first. Prove $P$ and $Q\vee R$ separately, each by the disjunction elimination rule on the premise, and combine them:

Both derivations establishCounting only applications of inference rules, each proof has nine steps: four conjunction elimination rule applications, two disjunction introduction rule applications, and three remaining applications. The first uses two conjunction introduction rule applications and one disjunction elimination rule; the second uses one and two, respectively. The second has two additional temporary-assumption lines, giving 14 displayed lines instead of 12, but assumptions are not additional inference applications. Its duplicated case analysis is exchanged for avoiding construction of the complete logical conjunction separately in both cases. In a proof tree it also repeats the use of the original premise.

Introduce the three logical implications from the outside in. Under assumptions $P\to Q$, $Q\to R$, and $P$, apply the implication elimination rule twice, then use assumption discharge in reverse order:

Thus

Under $P$, the first assumption yields $Q\to R$, while the second yields $Q$. Apply the implication elimination rule once more to obtain $R$, and discharge the three temporary assumptions:

The two uses of $P$ are permitted in ordinary natural deduction. Therefore

The premise turns an assumed $\neg P$ into a contradiction. Use the negation introduction rule to obtain $\neg \neg P$, then the supplied classical double-negation elimination rule:

Hence $\boxed{(\neg P\to \perp )⊢P}$. The final classical rule is essential: deriving $\neg \neg P$ alone is not yet a proof of $P$ in Intuitionistic propositional logic.

Assuming $\neg P$ lets the disjunction introduction rule produce the logical disjunction excluded by the premise. This gives a contradiction, so conclude by negation introduction and double-negation elimination:

ThusNo separate result about $Q$ or use of a derived De Morgan rule is needed.