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

The implication introduction rule assumes $ϕ$ locally, derives $ψ$ under that assumption, then concludes $ϕ \to ψ$ while discharging the temporary assumption.
The disjunction elimination rule uses $ϕ \lor ψ$ and two local cases: one derives a common conclusion $κ$ from $ϕ$ , and the other derives that same $κ$ from $ψ$ . It concludes $κ$ and discharges both case assumptions.
The negation introduction rule assumes $ϕ$ locally and derives logical falsity. Discharging that assumption gives $\neg ϕ$ .

The boxes delimit a subproof and identify the lifetime of its temporary assumptions. A result depending on a boxed assumption is available inside that box and its nested boxes; it cannot simply be exported outside. The enclosing rule specifies what may be exported and which assumptions are discharged. Other premises on which the derivation depends remain undischarged. This assumption discharge discipline distinguishes a conditional argument from an unconditional proof.

b

 0  0

Solution

 0  0

Derive each negated component in its own subproof, then combine them. Assumption lines below begin local scopes; the listed discharge ranges close those scopes.

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

Only the original premise remains open. No classical principle is needed for this direction of De Morgan's laws.

c

 0  0

Solution

 0  0

Assume the conjunction and obtain a contradiction in each of the two cases supplied by the premise:

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

The two case assumptions disappear at line 9, while the conjunction assumption remains available until line 10. The proof uses only the primitive rules printed in the paper.

d

 0  0

Solution

 0  0

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.

e

 0  0

Solution

 0  0

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.

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

a

Solution

b

Solution

c

Solution

d

Solution

e

Solution

 Ancestors (10)

 Discussion (0)

 Articles by others on the same topic (0)

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

 Discussion (0)  Subscribe (1)

 Discussion (0)