= Solution
Assume the existential statement and eliminate it using a fresh witness $u$. Let $A$ abbreviate $R(u,u)$. Instantiating its <universal quantification> at the witness itself gives two incompatible conditional requirements.
``
1 | ∃x ∀y ((R(x,y) → ¬R(y,y)) ∧ (¬R(y,y) → R(y,y))) assume
2 | | ∀y ((R(u,y) → ¬R(y,y)) ∧ (¬R(y,y) → R(y,y))) fresh witness
3 | | (A → ¬A) ∧ (¬A → A) ∀-elim, 2, y := u
4 | | A → ¬A ∧-elim-L, 3
5 | | ¬A → A ∧-elim-R, 3
6 | | | A assume
7 | | | ¬A →-elim, 6 and 4
8 | | | ⊥ ¬-elim, 6 and 7
9 | | ¬A ¬-intro, discharge 6–8
10 | | A →-elim, 9 and 5
11 | | ⊥ ¬-elim, 10 and 9
12 | ⊥ ∃-elim, 1, subproof 2–11
13 ¬∃x ∀y ((R(x,y) → ¬R(y,y)) ∧ (¬R(y,y) → R(y,y))) ¬-intro, discharge 1–12
``
The <contradiction> at line 12 contains no free witness variable, so the <existential quantifier elimination rule> meets its <eigenvariable condition>. This argument is already valid without <classical first-order logic> <double-negation elimination>.
Back to article page
