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.
asked Sep 26, 2015 at 17:10
Add a comment
|
5 Answers
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.
answered Sep 26, 2015 at 17:24
-
Can you explain where (2) comes from? You assume P(x) is true, under a free variable that is not quantified? I understand this is part of a proof by contradiction, I’m just not familiar with the ability to assert propositions for free variables. Why is that a feature of first order logic? Commented Feb 3 at 13:18
-
@JuliusH. It is assumed, the discharged at 5 by Neg Intro. Commented Feb 3 at 16:28
-
And yes, ND uses formulas and not only sentences (closed formulas). Commented Feb 3 at 16:29
To prove equivalence of P and Q we need to establish P → Q and Q → P.
Case ∀x ¬P(x) → ¬∃x P(x)
- Assume ∃x P(x).
- Eliminate the existential quantifier of (1) with x=x0: P(x0).
- Apply the universal quantifier to x0: ¬P(x0).
- Contradiction between (2) and (3): P(x) and ¬P(x).
- Therefore, the assumption in (1) must be incorrect: ¬∃x P(x).
Case ¬∃x P(x) → ∀x ¬P(x)
- Assume for some x0 that P(x0).
- Introduce the existential quantifier: ∃x P(x).
- Contradiction with the assumption.
- Therefore, ¬P(x0).
- 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. Commented Sep 27, 2015 at 4:42
-
@user21820 you're correct, I modified it. Thanks.– user2953Commented Sep 27, 2015 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. Commented Sep 27, 2015 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.– user2953Commented Sep 27, 2015 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)." Commented Sep 28, 2015 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. Commented Apr 22, 2019 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
answered Jun 14, 2019 at 15:33
-
I am just learning about these inference rules. The way I´ve been learning, there is an extra step that you seemed to have skipped. On line 2, you made the assumption that there is an arbitrary object a in the domain of discourse with the property P. Then you showed this leads to a contradiction. From this result, outside this subproof, you use negation introduction to infer ~P(a). But a is a temporary name used in the previous subproof. Isn't line 5 technically incorrect?– xouxCommented Jan 25, 2022 at 3:52
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.
