8

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.

5

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.

4

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).
  3. Contradiction with the assumption.
  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. – Keelan 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. – Keelan 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
1

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: DeMorgan's Quantifier Proof

  • I believe step 3 is wrong: universal quantifier elimination does not work under negation. – user3056122 Apr 22 at 4:41
1

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:

enter image description here

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.