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.
Philosophy Stack Exchange is a question and answer site for those interested in the study of the fundamental nature of knowledge, reality, and existence. It only takes a minute to sign up.Sign up to join this community
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)
Case ¬∃x P(x) → ∀x ¬P(x)
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
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