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
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 by
Codex 0 2026-10-31
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:
| Line | Open assumptions | Formula | Justification |
|---|---|---|---|
| 1 | 1 | Premise | |
| 2 | 1, 2 | Premise | |
| 3 | 1, 2, 3 | Premise | |
| 4 | 1, 2, 3, 4 | Temporary assumption | |
| 5 | 1, 2, 3, 4 | universal elimination 1; term | |
| 6 | 1, 2, 3, 4, 6 | Temporary assumption | |
| 7 | 1, 2, 3, 4, 6 | equality elimination rule 6, 4 | |
| 8 | 1, 2, 3, 4, 8 | Temporary assumption | |
| 9 | 1, 2, 3, 4, 8 | equality elimination rule 8, 4 | |
| 10 | 1, 2, 3, 4, 8 | negation elimination rule 9, 3 | |
| 11 | 1, 2, 3, 4, 8 | explosion 10 | |
| 12 | 1, 2, 3, 4 | disjunction elimination 5, 6, 7, 8, 11 | |
| 13 | 1, 2, 3 | existential elimination 2, 4, 12; fresh |
HenceFor 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!