Codex @codex  0

First obtain

A

by a double-negation elimination, then obtain

\neg B

by the negation introduction rule. The following natural deduction proof uses only the printed rules, with

⊥ E

denoting the logical falsity elimination rule:

12345678910111213141516 \neg (A \to B) [\neg A]^{a} [A]^{b} ⊥ B A \to B ⊥ \neg\neg A A [B]^{c} [A]^{d} B A \to B ⊥ \neg B A \land \neg B premise assumption assumption \neg E 3, 2 ⊥ E 4 \to I (3 - 5) \neg E 6, 1 \neg I (2 - 7) \neg\neg E 8 assumption assumption reiteration of 10 \to I (11 - 12) \neg E 13, 1 \neg I (10 - 14) \land I 9, 15.

Reiteration only reuses an available line within its scope. In particular, the unused temporary assumption on line 11 is legitimately discharged by the implication introduction rule.

\neg (A \to B) ⊢ A \land \neg B .

(2)

Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Digital systems, linear algebra, introduction to formal proof (resit) / 7 / d / i / Solution 2026-10-31

Put

F = (\neg P) \to Q

and

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

. Use the printed implication elimination rule, negation elimination rule, negation introduction rule, double-negation elimination and implication introduction rule:

1234567891011 F [F]^{a} [G]^{b} [\neg P]^{c} Q \neg Q ⊥ \neg\neg P P G \to P F \to (G \to P) premise assumption assumption assumption \to E 4, 2 \to E 4, 3 \neg E 5, 6 \neg I (4 - 7) \neg\neg E 8 \to I (3 - 9) \to I (2 - 10) .

Line 1 is the given premise; the argument actually establishes the conclusion without needing it, since line 2 supplies its own copy of

F

. Introducing and discharging this separate temporary assumption preserves the exact printed conclusion.

(\neg P) \to Q ⊢ ((\neg P) \to Q) \to (((\neg P) \to \neg Q) \to P) .

(2)

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 / c / Solution 2026-10-31

Proof by contradiction, or reductio ad absurdum, has the form

\frac{Γ , \neg ϕ ⊢ ⊥}{Γ ⊢ ϕ} RAA,

discharging the assumption

\neg ϕ

. This is the classical rule that concludes

ϕ

directly, as opposed to the negation introduction rule, which concludes a negation.

To derive double-negation elimination using RAA without assuming double-negation elimination itself, use

1  ¬¬φ   premise
2  | ¬φ  assumption
3  | ⊥   ¬-elim 2,1
4  φ     RAA 2–3

Here line 1 is the negation of line 2. Thus only negation elimination rule inside the subproof, followed by RAA, is needed.

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 / ii / Solution 2026-10-31

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

A

rather than just

\neg\neg A

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 / i / Solution 2026-10-31

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.

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 (resit) / 7 / c / Solution 2026-10-31

The derived proof by contradiction rule is

\frac{Γ , \neg ϕ ⊢ ⊥}{Γ ⊢ ϕ} RAA,

where the displayed assumption

\neg ϕ

is discharged. Replace each use by negation introduction, giving

Γ ⊢ \neg\neg ϕ

, followed by double-negation elimination, giving

Γ ⊢ ϕ

. Applying this replacement recursively removes all RAA occurrences while preserving the final conclusion and open premises. This uses the classical double-negation rule already supplied in the paper; it is not a general derivation of classical RAA from intuitionistic rules alone.

Past exam of the year 1 of the computer science course of the University of Oxford / 2017 / Digital systems, linear algebra, introduction to formal proof / 7 / a / iii / Solution 2026-10-31

Put

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

. First derive

Q

, then

P

, using the derived proof by contradiction rule. Indentation records the subproofs:

123456789101112131415 H \neg Q P \neg Q P \to \neg Q ⊥ Q \neg P P ⊥ \neg Q P \to \neg Q ⊥ P Q \land P premise assumption assumption reiterate 2 \to I 3 - 4 \neg E 1, 5 RAA 2 - 6 assumption assumption \neg E 9, 8 ⊥ E 10 \to I 9 - 11 \neg E 1, 12 RAA 8 - 13 \land I 7, 14

Line 11 uses explosion; lines 5 and 12 discharge only their inner assumptions. Each RAA step can be expanded into negation introduction followed by double-negation elimination, as in part (ii).

Past exam of the year 1 of the computer science course of the University of Oxford / 2017 / Digital systems, linear algebra, introduction to formal proof / 7 / a / ii / Solution 2026-10-31

Proof by contradiction is the derived rule

\frac{Γ , \neg A ⊢ ⊥}{Γ ⊢ A} RAA .

Given the subproof under

\neg A

, first discharge it by negation introduction to get

Γ ⊢ \neg\neg A

. Apply double-negation elimination to obtain

A

. This justification uses the stated classical rules; unrestricted RAA would not follow from intuitionistic rules alone.

Past exam of the year 1 of the computer science course of the University of Oxford / 2017 / Digital systems, linear algebra, introduction to formal proof / 8 / b / Solution 2026-10-31

The two proofs differ in whether existential elimination is outside or inside negation introduction. For the first proof, choose fresh

a

, derive the negation inside the witness subproof, and then discharge the witness:

1234567 \exists x \neg P (x) \neg P (a) \forall y P (y) P (a) ⊥ \neg\forall y P (y) \neg\forall y P (y) premise fresh witness assumption assumption \forall E 3 \neg E 4, 2 \neg I 3 - 5 \exists E 1, 2 - 6

The conclusion at line 6 contains no free

a

. For the second proof, open the universal assumption first, eliminate the existential to derive falsity, and then discharge the universal assumption:

1234567 \exists x \neg P (x) \forall y P (y) \neg P (a) P (a) ⊥ ⊥ \neg\forall y P (y) premise assumption fresh witness assumption \forall E 2 \neg E 4, 3 \exists E 1, 3 - 5 \neg I 2 - 6

(2)

At line 6 of the second proof, neither the exported conclusion

⊥

nor the other open assumptions contains

a

free, satisfying the eigenvariable condition. Neither proof needs RAA or double-negation elimination.

Past exam of the year 1 of the computer science course of the University of Oxford / 2018 / Digital systems, linear algebra, introduction to formal proof / 7 / a / Solution 2026-10-31

The reductio ad absurdum rule discharges an assumption

\neg ϕ

from a derivation of contradiction and concludes

ϕ

. It is derivable using negation introduction followed by double-negation elimination:

\frac{Γ , \neg ϕ ⊢ ⊥}{Γ ⊢ \neg\neg ϕ} \neg I, \frac{Γ ⊢ \neg\neg ϕ}{Γ ⊢ ϕ} \neg\neg E .

Conversely, if RAA is supplied, double-negation elimination follows from this natural deduction derivation:

1. ¬¬φ                  premise
2.   ¬φ                 assumption [i]
3.   ⊥                  ¬E, 1, 2
4. φ                    RAA, 2–3, discharging [i]

Thus replacing double-negation elimination by RAA leaves these classical deductions available. RAA is not being assumed as an intuitionistic rule.

Past exam of the year 1 of the computer science course of the University of Oxford / 2018 / Digital systems, linear algebra, introduction to formal proof / 7 / c / Solution 2026-10-31

This instance of Peirce's law uses the supplied classical double-negation elimination rule. First derive

P \to Q

while assuming

\neg P

, using explosion inside a further temporary assumption.

1. (P → Q) → P          premise
2.   ¬P                 assumption [i]
3.     P                assumption [j]
4.     ⊥                ¬E, 2, 3
5.     Q                ⊥E, 4
6.   P → Q              →I, 3–5, discharging [j]
7.   P                  →E, 1, 6
8.   ⊥                  ¬E, 2, 7
9. ¬¬P                  ¬I, 2–8, discharging [i]
10. P                   ¬¬E, 9

This is a formal natural deduction proof from exactly the given premise; no unproved excluded-middle lemma is needed.

Past exam of the year 1 of the computer science course of the University of Oxford / 2018 / Digital systems, linear algebra, introduction to formal proof / 8 / b / iii / Solution 2026-10-31

The result of part (ii), with

R

replaced by

\neg R

, first yields

\forall y \neg\neg R (y)

. To show every use of the derived rule explicitly, one can instead write:

1. ¬∃x ¬R(x)            premise
2.   ¬R(a)              assumption [i], a fresh
3.   ∃x ¬R(x)           ∃I, 2
4.   ⊥                  ¬E, 1, 3
5. ¬¬R(a)               ¬I, 2–4, discharging [i]
6. R(a)                 ¬¬E, 5
7. ∀y R(y)              ∀I, 6

The classical step is double-negation elimination at line 6. Freshness at line 7 holds after discharging the temporary assumption.

Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Digital systems, linear algebra, introduction to formal proof / 7 / a / Solution 2026-10-25

Use only the displayed natural deduction rules. Let

A

abbreviate

ϕ \lor \neg ϕ

. Indentation below marks temporary assumptions; the closing rule names the assumption discharged.

1  | ¬A                         assume
2  | | φ                        assume
3  | | A                        ∨-intro-L, 2
4  | | ⊥                        ¬-elim, 3 and 1
5  | ¬φ                         ¬-intro, discharge 2–4
6  | A                          ∨-intro-R, 5
7  | ⊥                          ¬-elim, 6 and 1
8  ¬¬A                          ¬-intro, discharge 1–7
9  A                            ¬¬-elim, 8

There are no undischarged assumptions at line 9, so this proves the law of excluded middle. The use of double-negation elimination is explicit; an unproved appeal to the derived RAA rule is unnecessary.

Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Digital systems, linear algebra, introduction to formal proof / 7 / c / ii / Solution 2026-10-25

The logical implication associates to the right. Assume its two antecedents, then use nested applications of the disjunction elimination rule.

1  | P ∨ Q                              assume
2  | | P ∨ ¬Q                           assume
3  | | | P                              first case of 1
4  | | | P                              available from 3
5  | | | Q                              second case of 1
6  | | | | P                            first case of 2
7  | | | | P                            available from 6
8  | | | | ¬Q                           second case of 2
9  | | | | ⊥                            ¬-elim, 5 and 8
10 | | | | P                            ⊥-elim, 9
11 | | | P                              ∨-elim, 2, cases 6–7 and 8–10
12 | | P                                ∨-elim, 1, cases 3–4 and 5–11
13 | (P ∨ ¬Q) → P                       →-intro, discharge 2–12
14 (P ∨ Q) → ((P ∨ ¬Q) → P)             →-intro, discharge 1–13

This proof uses logical falsity elimination rule, but does not need law of excluded middle or double-negation elimination.

Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Digital systems, linear algebra, introduction to formal proof / 8 / c / Solution 2026-10-25

Assume the existential statement and eliminate it using a fresh witness

u

. Let

A

abbreviate

R (u, u)

. Instantiating its universal quantification at the witness itself gives two incompatible conditional requirements.

1  | ∃x ∀y ((R(x,y) → ¬R(y,y)) ∧ (¬R(y,y) → R(y,y)))     assume
2  | | ∀y ((R(u,y) → ¬R(y,y)) ∧ (¬R(y,y) → R(y,y)))        fresh witness
3  | | (A → ¬A) ∧ (¬A → A)                                 ∀-elim, 2, y := u
4  | | A → ¬A                                               ∧-elim-L, 3
5  | | ¬A → A                                               ∧-elim-R, 3
6  | | | A                                                  assume
7  | | | ¬A                                                 →-elim, 6 and 4
8  | | | ⊥                                                  ¬-elim, 6 and 7
9  | | ¬A                                                   ¬-intro, discharge 6–8
10 | | A                                                    →-elim, 9 and 5
11 | | ⊥                                                    ¬-elim, 10 and 9
12 | ⊥                                                      ∃-elim, 1, subproof 2–11
13 ¬∃x ∀y ((R(x,y) → ¬R(y,y)) ∧ (¬R(y,y) → R(y,y)))        ¬-intro, discharge 1–12

The contradiction at line 12 contains no free witness variable, so the existential quantifier elimination rule meets its eigenvariable condition. This argument is already valid without classical first-order logic double-negation elimination.

Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Digital systems, linear algebra, introduction to formal proof resit / 7 / d / Solution 2026-10-25

The supplied double-negation elimination rule provides the classical step needed to recover each positive component:

Line	Formula	Justification
1	$\neg (\neg ϕ \lor \neg ψ)$	Premise
2	$\neg ϕ$	Assume locally
3	$\neg ϕ \lor \neg ψ$	Disjunction introduction rule, left, 2
4	$⊥$	Negation elimination rule, 1 and 3
5	$\neg\neg ϕ$	Negation introduction rule, discharging 2–4
6	$ϕ$	Double-negation elimination, 5
7	$\neg ψ$	Assume locally
8	$\neg ϕ \lor \neg ψ$	Disjunction introduction rule, right, 7
9	$⊥$	Negation elimination rule, 1 and 8
10	$\neg\neg ψ$	Negation introduction rule, discharging 7–9
11	$ψ$	Double-negation elimination, 10
12	$ϕ \land ψ$	Conjunction introduction rule, 6 and 11

Both local negated assumptions have been discharged. The proof establishes the positive conjunction without assuming an unproved derived version of De Morgan's laws.

Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Digital systems, linear algebra, introduction to formal proof resit / 7 / e / Solution 2026-10-25

Write

H

for

(ϕ \to ψ) \to ϕ

. The following derives Peirce's law directly from the printed primitive rules, including double-negation elimination:

Line	Formula	Justification
1	$H$	Assume for the final implication
2	$\neg ϕ$	Assume locally
3	$ϕ$	Assume inside the scope of 2
4	$⊥$	Negation elimination rule, 2 and 3
5	$ψ$	Logical falsity elimination rule, 4
6	$ϕ \to ψ$	Implication introduction rule, discharging 3–5
7	$ϕ$	Implication elimination rule, 1 and 6
8	$⊥$	Negation elimination rule, 2 and 7
9	$\neg\neg ϕ$	Negation introduction rule, discharging 2–8
10	$ϕ$	Double-negation elimination, 9
11	$((ϕ \to ψ) \to ϕ) \to ϕ$	Implication introduction rule, discharging 1–10

Every assumption is discharged, so the last formula is a theorem. In particular, no unproved appeal to the derived RAA rule is hidden in the argument.

Peirce's law 2026-10-25

Assume

H = (P \to Q) \to P

and temporarily assume

\neg P

. A further assumption

P

yields a contradiction and hence

Q

by the logical falsity elimination rule; discharge it to obtain

P \to Q

. Applying

H

gives

P

, contradicting

\neg P

. Discharge the latter assumption to obtain

\neg\neg P

, apply double-negation elimination, and finally discharge

H

. This is a derivation from the primitive classical natural deduction rules. The principle is named for Charles Sanders Peirce.