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

Table of contents
- Solution 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

, then apply disjunction elimination. In the first case equality elimination rule transfers

R (v)

to

R (c_{0})

; in the second it transfers

R (v)

to

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.

 Ancestors (11)

 View article source

 Discussion (0) New discussion

There are no discussions about this article yet.

 Articles by others on the same topic (0)

There are currently no matching articles.

  See all articles in the same topic Create my own version