# How to prove the tautology $\neg \forall{x} \exists{y} (Py \wedge \neg Px)$?

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.

-

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

-

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.

-
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

I'll consider Herbert Enderton, A Mathematical Introduction to Logic (2nd - 2001)).

The proof system [see page 112] is based on modus ponens as only rule of inference and :

The logical axioms are all generalizations of wffs of the following forms, where $x$ and $y$ are variables and $\alpha$ and $\beta$ are wffs:

1. Tautologies;

2. $\forall x \alpha \rightarrow \alpha^x_t$, where $t$ is substitutable for $x$ in $\alpha$;

3. $\forall x(\alpha \rightarrow \beta) \rightarrow (\forall x\alpha \rightarrow \forall x \beta)$;

4. $\alpha \rightarrow \forall x \alpha$, where $x$ does not occur free in $\alpha$.

We need also some provable equivalences; see Enderton, page 121 and page 130 :

(Q2A) -- $\vdash (\alpha \rightarrow \forall x \beta) \leftrightarrow \forall x (\alpha \rightarrow \beta)$, if $x$ does not occur free in $\alpha$

(Q2B) -- $\vdash (\alpha \rightarrow \exists x \beta) \leftrightarrow \exists x (\alpha \rightarrow \beta)$, if $x$ does not occur free in $\alpha$

(Q3A) -- $\vdash (\forall x \beta \rightarrow \alpha) \leftrightarrow \exists x (\beta \rightarrow \alpha)$, if $x$ does not occur free in $\alpha$

(Q3B) -- $\vdash (\exists x \beta \rightarrow \alpha) \leftrightarrow \forall x (\beta \rightarrow \alpha)$, if $x$ does not occur free in $\alpha$.

Proof

All the following steps are equivalences.

(1) $\exists y Py \rightarrow \exists y Py$ --- axiom 1 : it is an instance of the tautology : $\alpha \rightarrow \alpha$ [please, note that it is also : $\lnot \exists y Py \lor \exists y Py$, from which its "tautologuous" nature is still more evident]

(2) $\exists y Py \rightarrow \exists x Px$ --- renaming bound variables [see Theorem 241 (Existence of Alphabetic Variants), page 126]

(3) $\exists x(\exists y Py \rightarrow Px)$ --- by (Q2B), because $x$ is not free in $\exists y Py$

(4) $\exists x \forall y(Py \rightarrow Px)$ --- by (Q3B), because $y$ is not free in $Px$

(5) $\exists x \forall y \lnot (Py \land \lnot Px)$ --- by the tautological equivalence : $(p \rightarrow q) \leftrightarrow \lnot (p \land \lnot q)$

(6) $\lnot \forall x \exists y (Py \land \lnot Px)$ --- by the properties of quantifiers.

-