Deduce $ \forall x P(x) \vdash \exists xP(x) $

Question

Well it's a little awkward but how can I show this in a natural deduction proof?

$ \forall x P(x) \vdash \exists xP(x) $

I think one has too proof that with a proof by contradiction rule but since I cannot eliminate the $ \exists $ quantifier I am stuck. I know this is a quite simple example.

Any help would be appreciated!

Answer 1

It is a consequence of the rule of Universal Specification in standard first-order logic (FOL). Implicit is the assumption that the domain of discourse is non-empty.

In my own work, I never make use of this assumption. I usually make the domain of discourse explicit, e.g $\forall x\in\mathbb{R}: P(x)$ We know that $\exists x\in\mathbb{R}$, so we can infer that $\exists x\in\mathbb{R}:P(x)$.

Answer 2

For a proof with natural Deduction, we refer to Dirk van Dalen, Logic and Structure (5th ed - 2013) for the rules :

$$\frac{∀x \varphi(x) }{\varphi(t)} \text {∀E ; we require $t$ to be free for $x$ in $\varphi$ [page 86] }$$

$$\frac{\varphi[t/x] }{∃x \varphi} \text {∃I, with $t$ free for $x$ in $\varphi$ [page 93]}$$

---

The proof is quite simple :

(i) $∀xP(x)$ --- assumed

(ii) $P(z)$ --- from (i) by $∀E$, where $z$ is a variable not used in $P(x)$

(iii) $∃xP(x)$ --- from (ii) by $∃I$

$∀xP(x) ⊢ ∃xP(x)$

---

The above proof is consistent with the previous comments; see van Dalen [page 54] :

Definition 3.2.1 A structure is an ordered sequence $\langle A, R_1,\ldots, R_n, F_1,\ldots, F_m, \{ c_i |i \in I \} \rangle$, where $A$ is a non-empty [emphasis added] set. $R_1,\ldots, R_n$ are relations on $A$, $F_1,\ldots, F_m$ are functions on $A$, and the $c_i (i \in I)$ are elements of $A$ (constants).

---

In order to admit also empty domains, the above rules regarding quantifiers must be modified; see Free Logic.