Let abbreviate , and group the three equality alternatives on the left. The proof uses the binary disjunction elimination rule twice, so no unproved three-way derived rule is needed.
| Line | Formula | Justification |
|---|---|---|
| 1 | Premise | |
| 2 | Assume for the first implication | |
| 3 | Assume for the second implication | |
| 4 | Assume with fresh witness name | |
| 5 | Universal quantifier elimination rule, 1 | |
| 6 | Assume the first outer case | |
| 7 | Assume the first inner case | |
| 8 | Equality elimination rule, 7 and 4 | |
| 9 | Negation elimination rule, 2 and 8 | |
| 10 | Logical falsity elimination rule, 9 | |
| 11 | Assume the second inner case | |
| 12 | Equality elimination rule, 11 and 4 | |
| 13 | Disjunction introduction rule, left, 12 | |
| 14 | Disjunction elimination rule, 6, 7–10 and 11–13 | |
| 15 | Assume the second outer case | |
| 16 | Equality elimination rule, 15 and 4 | |
| 17 | Disjunction introduction rule, right, 16 | |
| 18 | Disjunction elimination rule, 5, 6–14 and 15–17 | |
| 19 | Existential quantifier elimination rule, 3 and 4–18 | |
| 20 | Implication introduction rule, discharging 3–19 | |
| 21 | Implication introduction rule, discharging 2–20 |
The witness name is absent from and from every assumption remaining after line 19, so the existential elimination is legal. Each equality is used in the forward direction supplied by the printed equality rule. The three named constants need not denote distinct objects: the case proof requires only that they exhaust the domain. This is existential quantification over a finitely named domain followed by exclusion of the first case.
Articles by others on the same topic
There are currently no matching articles.