= Solution
Introduce a fresh <existential witness> $v$ with $R(v)$. The universal premise gives $v=0\lor v=1$. In the first case, <equality elimination rule> gives $R(0)$. In the second, it gives $R(1)$, contradicting $\neg R(1)$; <explosion> then supplies the common case conclusion $R(0)$. Close both cases and then the witness scope:
\Table[
|| Line
|| Open assumptions
|| Formula
|| Justification
| 1
| 1
| $\forall x\, x=0\lor x=1$
| Premise
| 2
| 1, 2
| $\exists x\, R(x)$
| Premise
| 3
| 1, 2, 3
| $\neg R(1)$
| Premise
| 4
| 1, 2, 3, 4
| $R(v)$
| <Temporary assumption>
| 5
| 1, 2, 3, 4
| $v=0\lor v=1$
| <universal elimination> 1; term $v$
| 6
| 1, 2, 3, 4, 6
| $v=0$
| <Temporary assumption>
| 7
| 1, 2, 3, 4, 6
| $R(0)$
| <equality elimination rule> 6, 4
| 8
| 1, 2, 3, 4, 8
| $v=1$
| <Temporary assumption>
| 9
| 1, 2, 3, 4, 8
| $R(1)$
| <equality elimination rule> 8, 4
| 10
| 1, 2, 3, 4, 8
| $\bot$
| <negation elimination rule> 9, 3
| 11
| 1, 2, 3, 4, 8
| $R(0)$
| <explosion> 10
| 12
| 1, 2, 3, 4
| $R(0)$
| <disjunction elimination> 5, 6, 7, 8, 11
| 13
| 1, 2, 3
| $R(0)$
| <existential elimination> 2, 4, 12; fresh $v$
]
{title=A witness must yield the relation at zero}
Hence
$$
\boxed{R(0).}
$$
For both uses of <equality elimination rule>, the formula template is $R(z)$. At the final <existential elimination>, $v$ is fresh in all three original premises and absent from $R(0)$, so the <eigenvariable condition> holds. No additional assumption that the constants $0$ and $1$ denote distinct objects is needed.
Back to article page
