 Solution

ID: 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/8/c/solution

The premise limits every possible existential witness to the objects named by

c_{0}, c_{1}

; it does not assert that these constants name distinct objects. Instantiate it at a fresh witness

v

R (v)

R (c_{0})

; in the second it transfers

R (v)

R (c_{1})

, contradicting the assumed negation. The full natural deduction derivation is

123456789101112131415 \forall x (x = c_{0} \lor x = c_{1}) ∣ \neg R (c_{1}) ∣ ∣ \exists x R (x) ∣ ∣ ∣ R (v) ∣ ∣ ∣ v = c_{0} \lor v = c_{1} ∣ ∣ ∣ ∣ v = c_{0} ∣ ∣ ∣ ∣ R (c_{0}) ∣ ∣ ∣ ∣ v = c_{1} ∣ ∣ ∣ ∣ R (c_{1}) ∣ ∣ ∣ ∣ ⊥ ∣ ∣ ∣ ∣ R (c_{0}) ∣ ∣ ∣ R (c_{0}) ∣ ∣ R (c_{0}) ∣ (\exists x R (x)) \to R (c_{0}) \neg R (c_{1}) \to ((\exists x R (x)) \to R (c_{0})) premise assumption assumption witness assumption; v fresh \forall -elim 1 first case assumption = -elim 6, 4 second case assumption = -elim 8, 4 \neg -elim 9, 2 ⊥ -elim 10 \lor -elim 5, 6 - 7, 8 - 11 \exists -elim 3, 4 - 12 \to -intro 3 - 13 \to -intro 2 - 14

The sibling case subproofs end before the witness subproof closes. At line 13,

v

is absent from

R (c_{0})

and from all surrounding assumptions, so no witness escape occurs. The final two applications of implication introduction give

\forall x (x = c_{0} \lor x = c_{1}) ⊢ \neg R (c_{1}) \to (\exists x R (x)) \to R (c_{0}) .

The logical falsity elimination rule is needed to complete the contradictory second case with the same conclusion as the first case.

 New to topics? Read the docs here!