# Prove ¬∃x ∀y (E(x, y) ↔ ¬E(y, y)) given no premises

The only way I could think of to do this problem is reductio, but since the two biconditional terms are not contradictory, I am pretty stuck.

• Are you allowed to use the law of excluded middle? – user2953 Jun 2 '18 at 7:31
• I think you perform existential and universal elimination on your reductio premise and reach a contradiction – Schiphol Jun 2 '18 at 10:00

## 3 Answers

Smells like Russell's Paradox ...

Anyway, yes, you totally had the right idea: proof by contradiction! And the two conditionals will contradict as long as you instantiate them with the same constant a:

E(x,y) <-> ¬ E(y,y) is clearly false if x and y are the same, because then the statement becomes E(x,x) <-> ¬ E(x,x).

Whatever we choose for x, E(x,y) <-> ¬ E(y,y) is not true for all y, because it is not true for y = x.

• This is only correct in classical logics; see the discussion under my answer. – user2953 Jun 2 '18 at 23:19

Here is a proof using the law of excluded middle. After eliminating the existential quantifier to get x, apply the universal quantification on x itself to get E(x,x) ↔ ¬E(x,x). This is false if E(x,x) is true or false.

In 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.
``````
• It is unclear whether "no premises" means no law of excluded middle. If yes, I'll remove this. – user2953 Jun 2 '18 at 13:59
• Since you can prove LEM from no premises, you could always begin with that proof and satisfy the terms of the question. – Dennis Jun 2 '18 at 18:59
• @Dennis LEM does not hold in intuitionistic logic. – user2953 Jun 2 '18 at 19:01
• I was assuming OP was working in a classical system. Since most intro logic books assume such a system it seems likely, but you’re right that it wouldn’t be an intuitionistically valid proof. – Dennis Jun 2 '18 at 19:03