Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

I've been beating my head trying to prove the following tautology for some time:

$$ \therefore \neg \forall{x} \exists{y} (Py \wedge \neg Px)$$

I think there's some tricky intermediate step that I'm missing. Any help would be appreciated.

share|improve this question
add comment

2 Answers

Let's start from the equivalent form $$ \exists x \big( \forall y (\lnot Py \vee Px) \big), $$ where I've added a set of brackets for clarity. The inner statement contains a disjunction where one of the sentences is independent of $y$; therefore we can move that sentence out of the scope of the quantifier: $$ \exists x \big( Px \vee \forall y (\lnot Py) \big). $$ Now we again have a disjunction where the second sentence is independent of $x$, so we separate it in a similar way: $$ \exists x (Px) \vee \forall y (\lnot Py). $$ This is clearly a tautology, after changing the second half to the equivalent $\lnot\exists x(Px)$.

share|improve this answer
add comment

Let's rewrite it explicitely so the tautological character of the sentence can be easily seen. $$\exists_x \forall_y \, \neg P(y) \vee P(x)$$ It simply says that either ($\exists_x P(x)$) or ($\forall_y \,\neg P(y)$) holds for each formula P.

share|improve this answer
Right, but with that form the problem still remains: how do you prove it true? It's not hard to see that it is true, but to show as much? A little tougher. I'll see if reformulating it as above helps, however. –  arthur Jul 24 '12 at 5:24
Refolmulated statement is of the form $\neg q \vee q$ for $\forall_x P(x)$ replaced by $q$ and I think you could take it as an axiom (called law of excluded middle). –  Kuba Helsztyński Jul 24 '12 at 5:30
@arthur: How to formally prove it depends critically on which particular formal proof system for first-order-logic you want the proof to take place in. There are many equivalent ways to formalize proofs, and the proof of your property would look quite different in some of them. –  Henning Makholm Jul 24 '12 at 14:54
add comment

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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