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

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

• In my book, this is the definition of $\forall$. So in that case there it's nothing to prove. – Arthur Feb 16 at 23:39
• This is very dependent on the sort of deduction system you're working with (Natural Deduction?, or a Hilbert system?, etc.) and the precise definitions you're working with. For contrast, you can see a proof in a particular Hilbert system here in the Metamath Proof Explorer. Unfortunately, expanding that particular proof down to axioms and definitions requires about 100 axioms/other small theorems being cited. – Mark S. Feb 17 at 15:23

$$\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}$$
• What does it mean to just have $a$ by itself? How are you going from $\neg P(a)$ assumption using $a$ to $\exists x \ \neg P(x)$ using $x$ as opposed to $\exists a \ \neg P(a)$? What rules are you using for the quantifiers? – user525966 Feb 17 at 0:13
• @user525966 The '$a$' on line 3 is a way of introducing a constant to take on the role of any arbitrary object in the domain. So, line 3 is basically saying 'Let $a$ be an arbitrary object'. So, it is not really a claim .. but rather an introduction of that constant just so we can talk about arbitrary objects of the domain. This is exactly how some Fitch systems formalize universal proofs ... but apparently not the one you are using? (There are many different ways to formalize these rules, even among Fitch systems). How do you do a universal proof in the system you are wrking with? – Bram28 Feb 17 at 0:31