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))

  • 1
    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
  • 1
    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.
    – jhk999
    Oct 20 '16 at 8:26


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.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.