Is there a proof of $\lnot \forall x, P(x) \iff \exists x, \lnot P(x)$

first-order-logicformal-proofslogicpredicate-logicquantifiers

I am interested in how one would formally prove:

$\lnot \forall x, P(x) \iff \exists x, \lnot P(x)$

I realize that it's basically saying that:

$\lnot(P(x_0) \land P(x_1) \land … \land P(x_n)) \iff \lnot P(x_0) \lor \lnot P(x_1) \lor … \lor \lnot P(x_n)$

Which is an "intuitive" proof assuming we already accept De Morgan's, but I am curious if there is a formal way to prove it (e.g. Fitch-style).

Best Answer

Fitch style proof:

\begin{array}{lll} 1&\neg \forall x \ P(x) & Assumption\\ 2&\quad \neg \exists x \ \neg P(x)&Assumption\\ 3&\quad \quad a&\\ 4&\quad \quad \quad \neg P(a) & Assumption\\ 5&\quad \quad \quad \exists x \ \neg P(x)&\exists \ Intro \ 4\\ 6&\quad \quad \quad \bot& \bot \ Intro \ 2,5\\ 7&\quad \quad \neg \neg P(a)& \neg \ Intro \ 4-6\\ 8& \quad \quad P(a)& \neg \ Elim \ 7\\ 9&\quad \forall x \ P(x) & \forall \ Intro \ 3-8\\ 10&\quad \bot & \bot \ Intro \ 1,9\\ 11&\neg \neg \exists x \ \neg P(x)&\neg \ Intro \ 2-10\\ 12&\exists x \ \neg P(x)&\neg \ Elim \ 11\\ \end{array}

Conceptual explanation: the basic strategy is to prove this by a proof by contradiction. That is, if it is not the case that there is some non-P, then everything is a P, which contradicts the assumption that not everything is a P.

Related Question