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

Abbreviate

H = (\neg P) \to Q

and

K = (\neg P) \to \neg Q

. Use the primitive natural deduction rules, including double-negation elimination:

1  H             premise
 2  | H          assumption
 3  | | K        assumption
 4  | | | ¬P     assumption
 5  | | | Q      →-elim 2,4
 6  | | | ¬Q     →-elim 3,4
 7  | | | ⊥      ¬-elim 5,6
 8  | | ¬¬P      ¬-intro 4–7
 9  | | P        ¬¬-elim 8
10  | K → P      →-intro 3–9
11  H → (K → P)  →-intro 2–10

The outer premise is redundant: the proof uses the locally assumed

H

, so the conclusion is already a theorem. Keeping the redundant premise is allowed. The successive discharges give $((\neg P) \to Q) \to (((\neg P) \to \neg Q) \to P)$ with exactly the requested assumption scopes.

ii

 0  0

Solution

 0  0

First derive

A

by double-negation elimination, then derive

\neg B

by negation introduction. The logical falsity elimination rule is used only inside the attempt to derive

A

1  ¬(A → B)  premise
 2  | ¬A     assumption
 3  | | A    assumption
 4  | | ⊥    ¬-elim 3,2
 5  | | B    ⊥-elim 4
 6  | A → B  →-intro 3–5
 7  | ⊥      ¬-elim 6,1
 8  ¬¬A      ¬-intro 2–7
 9  A        ¬¬-elim 8
10  | B      assumption
11  | | A    assumption
12  | | B    reiteration 10
13  | A → B  →-intro 11–12
14  | ⊥      ¬-elim 13,1
15  ¬B       ¬-intro 10–14
16  A ∧ ¬B   ∧-intro 9,15

Reiteration at line 12 merely uses an assumption that remains in scope. The final $A \land \neg B$ follows by conjunction introduction. This explicitly supplies the classical step needed to obtain