# How would you go on proving Law of Excluded Middle with Quantifiers?

The following obviously follows true from no premises, but I can't seem to find a formal proof to it unfortunately.

∃x ∀y (¬P (y) ∨ P (x))

• That is an odd way of formalising the LEM. I would write ∀x,P: ¬P(x) ∨ P(x) or even ∀p: p ∨ ¬p. You don't prove it, is an axiom (in some logic systems; not in all).
– user2953
Oct 20 '16 at 8:13
• You are right but I thought adding the existential quantifier would be fairly simple this is true when x=y. I somehow couldn't do this unfortunately. Oct 20 '16 at 8:26

Hint

We need LEM : ∀zP(z) ∨ ¬∀zP(z)

Proof by cases (or -elim) :

1) ∀zP(z) --- assumed [a]

2) P(x) --- by -elim

3) ¬P(y) ∨ P(x) --- by -intro

4) ∃y∀x (¬P(y) ∨ P(x)) --- by -intro followed by -intro

5) ¬∀zP(z) --- assumed [b]

6) ∃z¬P(z) --- equivalent

7) ¬P(y) --- assumed [c] for -elim

8) ¬P(y) ∨ P(x) --- by -intro

9) ∃y∀x (¬P(y) ∨ P(x)) --- now we may discharge [c] by -elim from 6)

From 4) and 9) we conclude with :

∃y∀x (¬P(y) ∨ P(x))

by -elim with LEM.

We may "verify" it through some equivalences. Consider :

∀x (A ∨ P(x)) ↔ (A ∨ ∀x P(x));

with it, we may rewrite the original formula : ∃x ∀y (¬P (y) ∨ P (x)) as :

∃x (∀y ¬P (y) ∨ P (x)).

Then we need the equivalence :

∃x (A ∨ P (x)) ↔ (A ∨ ∃x P(x))

and we rewtite the last formula as :

∀y ¬P (y) ∨ ∃x P (x))

which in turn is equivalent to :

¬ ∃y P (y) ∨ ∃x P (x) --- LEM.