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

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.

ii

 0  0

Solution

 0  0

Let

H

abbreviate the universal premise, and put

K = Q (c_{1}) \lor Q (c_{2})

. The constants need not denote distinct elements. Use a fresh witness

u

for the existential, then the justified three-case disjunction elimination from (i):

1  ∀x (x=c0 ∨ x=c1 ∨ x=c2)              premise H
2  | ¬Q(c0)                            assume
3  | | ∃x Q(x)                         assume
4  | | | Q(u)                          fresh witness for 3
5  | | | u=c0 ∨ u=c1 ∨ u=c2            ∀-elim, 1
6  | | | | u=c0                        first case
7  | | | | Q(c0)                       =-elim, 6 and 4
8  | | | | ⊥                           ¬-elim, 7 and 2
9  | | | | K                           ⊥-elim, 8
10 | | | | u=c1                        second case
11 | | | | Q(c1)                       =-elim, 10 and 4
12 | | | | K                           ∨-intro-L, 11
13 | | | | u=c2                        third case
14 | | | | Q(c2)                       =-elim, 13 and 4
15 | | | | K                           ∨-intro-R, 14
16 | | | K                             3-cases, 5, subproofs 6–9, 10–12, 13–15
17 | | K                               ∃-elim, 3, subproof 4–16
18 | (∃x Q(x)) → K                     →-intro, discharge 3–17
19 ¬Q(c0) → ((∃x Q(x)) → K)             →-intro, discharge 2–18

Equality elimination rule has exactly the forward orientation displayed in Figure 4: substitute the equal constant for