E(x,y) <-> ¬ E(y,y) явно ложно, если x и y совпадают, потому что тогда утверждение становится E(x,x) <-> ¬ E(x,x).
Что бы мы ни выбрали для x, E(x,y) <-> ¬E(y,y) не верно для всех y, потому что это неверно для y = x.
Вот доказательство с использованием закона исключенного третьего. После устранения квантора существования, чтобы получить x , примените универсальную количественную оценку к самому x , чтобы получить E(x,x) ↔ ¬E(x,x). Это неверно, если E(x,x) истинно или ложно.
В Коке:
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.
пользователь2953
Схипхол