# 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

## 1 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.

• You just need to specify what you are proving to get my up vote. Struggling students will not know and this will be confusing to them as is. – Git Gud Feb 17 at 0:00
• 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
• @Bram28 Wish I knew! I am trying to learn it. I made a new question about this. – user525966 Feb 17 at 0:33
• @user525966 Ah! Are you not using a book? – Bram28 Feb 17 at 0:43