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))
Philosophy Stack Exchange is a question and answer site for those interested in the study of the fundamental nature of knowledge, reality, and existence. It only takes a minute to sign up.Sign up to join this community
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.