Krdytkyu

Negating a universal quantifier gives the existential quantifier, and vice versa:

$neg forall x = exists x \
neg exists x = forall x$

Why is this, and is there a proof for it (is it even possible to prove it, or is it just an axiom)? Intuitively, I would think that negating "for all" would give "none," or even "not for all," and that negating "there exists" would give "there does not exist".

The following two statements are equivalent:

"It is not true that all men have red hair."

"There exists at least one man who does not have red hair."

Hence $negforall x varphi$ is the same as $exists x negvarphi$.

The following are equivalent:

"It is not true that some men have green hair."

"All men have non-green hair."

Hence $neg exists x varphi$ is the same as $forall x negvarphi$.

However, the form in which you've written them is not correct (as pointed out in Daniel Fischer's comment).

I will answer in a way that will likely add confusion, but I hope shows why this type of question should not be seen as too obvious and easy. I apologise in advance.

One question that comes up is "what does it mean to assert $forall x (P(x))$ when there are infinite x?" Why do students ask such a silly question? Because one way to answer it is to say "it is a fact that all x obey P" or "it is known that all x obey P" or "it has been shown P(x) for all x" or "for every x we can prove P(x)". Something like that is what a lot of students have in mind, and when one is dealing with infinities, things like knowing or proving may never get finished.

Similarly, we can ask what it means to show $exists x (P(x))$. One way that students will often think about this is that showing that is giving a particular x that obeys P.

Now, if these are the things the student is thinking, then it certainly seems reasonable to ask the question of the OP. Even if we can assert that "it is known that not all x obey P" or worse, that "for every x we cannot prove P(x)", this does not mean we have given a particular x that obeys P! So how can we assert existence here? What if we just don't know?

Of course, the answer is that there are different, completely valid ways to answer this. On one side, you have the constructivists who will smile at these questions, pat you on the shoulder, and tell you "good questions, all" as they lead you off on explanations of the meaning of truth and accessible knowledge. On another side, you have the classicists, who will try to help this poor student understand that there is much more to truth than knowledge and proof, and try to build in that student reasons why bivalent reasoning about these kinds of things is still important and how can reach assertions of existence nonconstructively.

These are both valid paths one may walk down in the philosophy of mathematics. They offer different ways to understand the meaning of assertions, and it often seems like both sides are talking past each other when they are often just talking about different things entirely. A curious student might want to get familiar with both sides, and learn the ways each approach formal manipulation.

A noncurious student, though, should probably just learn the rule and move on. Beyond here, there be dragons.

Answer to the question in the middle of the OP: in terms of formal logic this is an axiom, or to put it better it is the definition of one quantifier in terms of the other.

For example, one may take $forall$ as an undefined symbol and then define $exists x,P(x)$ to mean $negforall x,(neg P(x))$.

So from the strictly formal point of view there is no question to answer here, it's just the definition. On the other hand, we do want logic to reflect accepted and understood modes of reasoning, so examples such as those given in other answers and comments are important.

This was already observed by Aristoteles in his square of opposition, looking at the contradictory path:

But my question is, is this a property of classical logic, or have non-classical logics also such quantifiers? Unfortunately, for example in inituitionistc logic, we only have the following directions which are generally valid:

∃x¬φ → ¬∀xφ

∀x¬φ → ¬∃xφ

¬∃xφ → ∀x¬φ

But this direction is not generally valid, picked from the wiki page about interdefinability:

¬∀xφ → ∃x¬φ

The last formula might fail since the forall might be in a possible world with a greater domain than the exists.