Proof for Negation of existential quantifier : Formal Deduction && Predicate Logic

Question

Prove in natural deduction (Negation of existential quantifier):

• ∀x ¬P(x) ⊢ ¬∃x P(x)

Inference rules:

• (∀−) If $Σ ⊢ ∀xA(x)$, then $Σ ⊢ A(t)$ where $t$ is any term.
• (∀+) If $Σ ⊢ A(u)$ and $u$ does not occur in $Σ$, then $Σ ⊢ ∀xA(x)$.
• (∃−) If $Σ, A(u) ⊢ B$ and $u$ does not occur in $Σ$ or $B$, then $Σ, ∃xA(x) ⊢ B$.
• (∃+) If $Σ ⊢ A(t)$ then $Σ ⊢ ∃xA'(x)$ where $A'(x)$ results from $A(t)$ by replacing some (not necessarily all) occurrences of $t$ by $x$.
• (¬−) If $Σ,¬A ⊢ B$ and $Σ,¬A ⊢ ¬B$, then $Σ ⊢ A$.
• (¬+) If $Σ,A ⊢ B$ and $Σ,A ⊢ ¬B$, then $Σ ⊢ ¬A$.

How do I start with this proof?

Answer 1

The following is a proof in natural deduction of $\forall x \lnot P(x) \vdash \lnot \exists x P(x)$:

$$\dfrac{\dfrac{[\exists x P(x)]^* \qquad \dfrac{[P(x)]^{**} \qquad \dfrac{\forall x \lnot P(x)}{\lnot P(x)}\forall_\text{elim}}{\bot}\lnot_\text{elim}}{\bot}\exists_\text{elim}^{**}}{\lnot \exists x P(x)}\lnot_\text{intro}^*$$

where $[A]^*$ means that the assumption $A$ has been discharged by the rule $*$.

Answer 2

Here's a semi-formal proof. Try to build your proof along that.

Assume $\exists x\,P(x)$. For such an $x$, we have $P(x)$. On the other hand, specialization from $\forall x\,\neg P(x)$ gives us $\neg P(x)$. So we obtain $P(x)\land \neg P(x)$. Conclude.