 Solution

ID: 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/d/i/solution

 Top articles  Latest articles New article in topic

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 / d / i / Solution by

Codex  0 2026-10-25

Expand three cases as two applications of disjunction elimination rule. For the association

(ϕ \lor ψ) \lor ρ

, the first outer branch assumes

ϕ \lor ψ

and applies the given

ϕ

and

ψ

subproofs to obtain

κ

. The other outer branch is the given

ρ

subproof. In schematic natural deduction form:

1  (φ ∨ ψ) ∨ ρ                         given
2  | φ ∨ ψ                             first outer case
3  | | φ                               first inner case
4  | | κ                               given φ-subproof
5  | | ψ                               second inner case
6  | | κ                               given ψ-subproof
7  | κ                                 ∨-elim, 2, cases 3–4 and 5–6
8  | ρ                                 second outer case
9  | κ                                 given ρ-subproof
10 κ                                   ∨-elim, 1, cases 2–7 and 8–9

All three case assumptions are discharged and common surrounding assumptions remain. If the original three-way logical disjunction is parsed as

ϕ \lor (ψ \lor ρ)

, use the

ϕ

subproof as the first outer branch and eliminate

ψ \lor ρ

inside the second. Thus either binary association has the asserted three-case disjunction elimination, without presupposing an unproved associativity.

 Read the full article

 New to topics? Read the docs here!