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

Use natural deduction with labelled temporary assumptions. Assume $\neg P\to \neg Q$ under label $a$, then $\neg P\to Q$ under label $b$, then $\neg P$ under label $c$. Two applications of the modus ponens rule give $\neg Q$ and $Q$. The negation elimination rule gives $\perp$, and the supplied reductio ad absurdum rule discharges $c$ to conclude $P$.

Discharge $b$ using the implication introduction rule, obtaining $(\neg P\to Q)\to P$ under $a$. Discharge $a$ with the implication introduction rule, obtainingAll three temporary assumptions have now been discharged; no premise remains.

Keep the four given premises in context and assume $P$ under label $a$. The modus ponens rule applied to the first two premises gives $Q\vee R$ and $\neg S$. Apply the disjunction elimination rule to $Q\vee R$ as follows.

Under a case assumption $Q$, the premise $Q\to S$ gives $S$ by the modus ponens rule. Together with $\neg S$, the negation elimination rule gives $\perp$, and the supplied logical falsity elimination rule gives $R$. Under the other case assumption $R$, the required conclusion $R$ is already available. Discharge both case assumptions with the disjunction elimination rule to conclude $R$.

Finally discharge $a$ with the implication introduction rule, giving $P\to R$. The premise $S\to Q$ is not needed: a derivation is permitted to leave a premise unused.

Use the disjunction elimination rule on the outer disjunction. In its left branch, assume $P\vee Q$ and apply the disjunction elimination rule again: from a case assumption $P$, the disjunction introduction rule gives $P\vee R$; from a case assumption $Q$, the premise $Q\to R$ and the modus ponens rule give $R$, then the disjunction introduction rule gives $P\vee R$. Discharging those two inner case assumptions yields $P\vee R$ under the left outer branch.

In the right outer branch, assume $R\vee S$. A case assumption $R$ gives $P\vee R$ by the disjunction introduction rule. A case assumption $S$, together with the premise $\neg S$, gives $\perp$ by the negation elimination rule, and then $P\vee R$ by logical falsity elimination rule. Discharge these inner case assumptions with the disjunction elimination rule.

Both outer branches now have the same conclusion. Discharge the two outer case assumptions with the disjunction elimination rule to obtain $P\vee R$ under exactly the stated premises.

Assume $E\to G$ under label $a$, $F\to G$ under label $b$, and $E\vee F$ under label $c$. A temporary case assumption $E$ gives $G$ by the modus ponens rule using $a$. A temporary case assumption $F$ gives $G$ by the modus ponens rule using $b$. The disjunction elimination rule discharges these case assumptions and concludes $G$ under $a,b,c$.

Apply the implication introduction rule three times, discharging $c$, then $b$, then $a$. The resulting theorem isThe displayed parentheses make explicit the right association of the source formula.

Let $N(\varphi ,\psi )$ abbreviate $\neg \varphi \wedge \neg \psi$. Suitable rules areTheir derivations require no new axiom. For introduction, apply the conjunction introduction rule to the two premises, obtaining $\neg \varphi \wedge \neg \psi$, which is exactly the abbreviation. For left and right elimination, unfold the abbreviation and apply the corresponding conjunction elimination rule. These are therefore derived rules for the NOR connective.

An equivalent subproof presentation of introduction permits one subproof from assumption $\varphi$ to $\perp$ and another from assumption $\psi$ to $\perp$: use the negation introduction rule to discharge each assumption, then apply the conjunction introduction rule. If elimination is desired in contradiction form, combine the left projection with $\varphi$, or the right projection with $\psi$, using the negation elimination rule. All these presentations reduce directly to the permitted rules.

Write $D(\varphi ,\psi )=\neg (\neg \varphi \wedge \neg \psi )$. We derive the two disjunction introduction rules and the disjunction elimination rule without using any disjunction rule inside the derivations.

For left introduction, start with $\varphi$ and temporarily assume $\neg \varphi \wedge \neg \psi$. The conjunction elimination rule gives $\neg \varphi$, and the negation elimination rule gives $\perp$. Discharge the temporary conjunction by the negation introduction rule, concluding $D(\varphi ,\psi )$. For right introduction, start with $\psi$ and use the right conjunction elimination rule to obtain $\neg \psi$ instead. Thus either input derives the required encoded disjunction.

For elimination, suppose $D(\varphi ,\psi )$ is available, together with a derivation of $\kappa$ from an additional assumption $\varphi$ and a derivation of $\kappa$ from an additional assumption $\psi$. Keep their common external context fixed. Temporarily assume $\neg \kappa$ under label $a$. Temporarily assume $\varphi$ under label $b$ and insert the supplied first branch derivation to obtain $\kappa$. Negation elimination rule gives $\perp$, so negation introduction rule discharges $b$ and gives $\neg \varphi$. Repeat with a temporary assumption $\psi$ under label $c$ and the supplied second branch derivation, discharging $c$ to obtain $\neg \psi$.

Conjunction introduction rule now gives $\neg \varphi \wedge \neg \psi$. Its negation $D(\varphi ,\psi )$ gives $\perp$ by negation elimination rule. The supplied reductio ad absurdum rule discharges $a$ and yields $\kappa$. This discharges the two branch assumptions as required and proves the encoded elimination rule. Its last step uses classical propositional logic; the same encoded elimination principle is not generally available in Intuitionistic propositional logic.