Demostrar ¬∃x ∀y (E(x, y) ↔ ¬E(y, y)) sin premisas

Huele a la paradoja de Russell...

De todos modos, sí, tenías toda la idea correcta: ¡prueba por contradicción! Y los dos condicionales se contradirán siempre que los instancias con la misma constante a:

E(x,y) <-> ¬ E(y,y) es claramente falsa si x e y son iguales, porque entonces el enunciado se convierte en E(x,x) <-> ¬ E(x,x).

Lo que sea que elijamos para x, E(x,y) <-> ¬ E(y,y) no es cierto para todo y, porque no es cierto para y = x.

Aquí hay una prueba usando la ley del tercero excluido. Después de eliminar el cuantificador existencial para obtener x , aplique la cuantificación universal sobre x para obtener E(x,x) ↔ ¬E(x,x). Esto es falso si E(x,x) es verdadero o falso.

En coq:

Variable P : Prop -> Prop -> Prop.
Axiom LEM : forall p, p \/ ~p.

Goal ~exists x, forall y, (P x y -> ~P y y) /\ (~P y y -> P x y).
intro.
elim H.
intros.
assert (P x x \/ ~P x x) by apply LEM.
elim H1; intro.
apply H0 with x; assumption.
apply H0 with x; apply H0; assumption.
Qed.