Solution

ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2013/digital-systems-linear-algebra-introduction-to-formal-proof/8/b/iii/solution

Introduce a fresh existential witness with . The universal premise gives . In the first case, equality elimination rule gives . In the second, it gives , contradicting ; explosion then supplies the common case conclusion . Close both cases and then the witness scope:
Table 1.
A witness must yield the relation at zero
.
LineOpen assumptionsFormulaJustification
11Premise
21, 2Premise
31, 2, 3Premise
41, 2, 3, 4Temporary assumption
51, 2, 3, 4universal elimination 1; term
61, 2, 3, 4, 6Temporary assumption
71, 2, 3, 4, 6equality elimination rule 6, 4
81, 2, 3, 4, 8Temporary assumption
91, 2, 3, 4, 8equality elimination rule 8, 4
101, 2, 3, 4, 8negation elimination rule 9, 3
111, 2, 3, 4, 8explosion 10
121, 2, 3, 4disjunction elimination 5, 6, 7, 8, 11
131, 2, 3existential elimination 2, 4, 12; fresh
Hence
For both uses of equality elimination rule, the formula template is . At the final existential elimination, is fresh in all three original premises and absent from , so the eigenvariable condition holds. No additional assumption that the constants and denote distinct objects is needed.

New to topics? Read the docs here!