# How does one prove De Morgan's laws for quantifiers?

One of De Morgan's laws state that ¬∃x P(x) is equivalent to ∀x ¬P(x), but how would one go about formally proving this?

Numerous attempts to find a solution have been futile, even proofwiki.org does not have a solution for this.

Using Natural Deduction rules.

First part :

1) ¬∃xP(x) --- premise

2) P(x) --- assumed [a]

3) ∃xP(x) --- from 2) by ∃-intro

4) --- contradiction, from 1) and 3)

5) ¬P(x) --- from 2) and 4) by ¬-intro (or →-intro, if we agree on the abbreviation ¬ϕ : = ϕ → ⊥), discharging [a]

6) ∀x ¬P(x) --- from 5) by ∀-intro, where x does not occur free in any undischarged assumptions.

Thus, from 1)-6) we have : ¬∃xP(x) ⊢ ∀x ¬P(x) and with a final application of →-intro we conclude with :

⊢ ¬∃xP(x) → ∀x ¬P(x).

The second part is similar, derive : ∀x ¬P(x) ⊢ ¬∃xP(x) and conclude by →-intro with :

⊢ ∀x ¬P(x) → ¬∃xP(x).

Finally, apply ↔-intro.

To prove equivalence of P and Q we need to establish P → Q and Q → P.

Case ∀x ¬P(x) → ¬∃x P(x)

1. Assume ∃x P(x).
2. Eliminate the existential quantifier of (1) with x=x0: P(x0).
3. Apply the universal quantifier to x0: ¬P(x0).
4. Contradiction between (2) and (3): P(x) and ¬P(x).
5. Therefore, the assumption in (1) must be incorrect: ¬∃x P(x).

Case ¬∃x P(x) → ∀x ¬P(x)

1. Assume for some x0 that P(x0).
2. Introduce the existential quantifier: ∃x P(x).
4. Therefore, ¬P(x0).
5. Introduce the universal quantifier: ∀x ¬P(x).
• You're using the wrong symbol. "⊨" is semantic entailment, but you are proving syntactic derivability just like Mauro. For (classical) first-order logic these are equivalent, but not in other logics. – user21820 Sep 27 '15 at 4:42
• @user21820 you're correct, I modified it. Thanks. – user2953 Sep 27 '15 at 9:22
• Great! But it's not clear what your step 1 in the second case really means. Technically you want to universally quantify x0, but you write "for some x0". Depending on the details of the deductive rules you are using, this may require some restrictions on when you can introduce the universal quantifier. – user21820 Sep 27 '15 at 13:17
• @user21820 it's very clear. It's a simple proof by contradiction. If there were an x0 such that P(x0), that would be a contradiction with the premise. Therefore, for all x, ~P(x). If you think that this is not allowed, please provide references. – user2953 Sep 27 '15 at 13:49
• The underlying argument is fine, which is why I didn't say it was wrong. All I was saying is that semantically you want a universal quantification for x0, but the phrasing you use ("for some") is quite contrary to that intended meaning. Your comment actually does not follow what you wrote, since in saying "if there were an x0" you already have the existential quantification in the assumption, which is what you cannot have. Rather you have to take any arbitrary variable x0, and then the assumption is just P(x0) with no quantification. Better: "1. Take a fresh variable x0. 2. Assume P(x0)." – user21820 Sep 28 '15 at 1:20

Surely the accepted answer relies on having the premise ¬∃xP(x). DeMorgan's laws are tautologies, so you should be proving

: ¬∃xP(x) ↔ ∀x ¬P(x)

I just wrote this proof, which I think is right: • I believe step 3 is wrong: universal quantifier elimination does not work under negation. – user3056122 Apr 22 '19 at 4:41

The following proof is similar to those provided but adds Fitch-style formatting in a proof checker with reference to the forallx text for more information: The inference rules used were

• existential introduction (∃I, Section 32.2)
• universal introduction (∀I, Section 32.4)
• universal elimination (∀E, Section 32.1)
• negation introduction (¬I, Section 15.7)
• negation elimination (¬E, Section 15.7)
• biconditional introduction (↔I, Section 15.5)

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Fall 2019. http://forallx.openlogicproject.org/forallxyyc.pdf

In case you are looking for not just a quick proof, but an actual extended explanation, I have made a video of myself teaching these proofs.

https://youtu.be/0HNZ2hXtecs

New contributor
William Rose is a new contributor to this site. Take care in asking for clarification, commenting, and answering. Check out our Code of Conduct.