# How to prove “basic” identities in first order logic?

On the Wikipedia page for First-order logic, there is a list of Provable Identities. Although they seem very basic, I can't find anyone giving a formal proof of them.

In particular, consider one direction of one of these identities:

$$\lnot \forall a. P(a) \to \exists b. \lnot P(b)$$

What are some strategies to prove this statement -- that is, how do I 'work' with the negation of a quantifier?

• @Lucky Using what deduction system? – Git Gud Nov 10 '13 at 17:04
• You could use the method of analytic tableaux. – Shaun Nov 10 '13 at 17:05
• That Wikipedia article is fairly awful. I would advise you not to take it too seriously. – dfeuer Nov 10 '13 at 17:06
• Your link is titled "Probable" and the URL is titled "Provable. There is a huge difference between provable and probable. Many probable things turn out to be unprovable, and many provable things are also improbable things. – Asaf Karagila Nov 10 '13 at 17:14
• It's helpful to know that "$\forall$" can be defined as "$\neg\exists\neg$", presuming classical logic. – Malice Vidrine Nov 10 '13 at 18:12

$$\lnot \forall a, P(a) \implies \exists b : \lnot P(b) \\ \iff \\ \exists a : \lnot P(a) \implies \exists b : \lnot P(b)$$

QED

You should immediately see why this is true by understanding the meaning of the symbols.

For example, the first part says:

not (for all $a$, $P(a)$), which if you can't negate that in English, can be rewritten:

$$\lnot (\bigwedge_{a \in A} P(a))$$ which equals, using DeMorgan's :

$$\bigvee_{a \in A} \lnot P(a)$$

In other words, converting that back to English, there exists a $b$ such that $\lnot P(b)$, then to math symbols, an implication of the above expression is:

$$\exists b : \lnot P(b)$$

QED