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 can not eliminate the $ \exists $ quantifier I am stuck. I know this is a quite simple example.

Any help would be appreciated!

  • 3
    $\begingroup$ The empty model doesn't satisfy the corresponding implication. $\endgroup$ – Berci Oct 16 '14 at 17:33
  • 3
    $\begingroup$ I don't think you can: the condition $\;\forall\,x\;P(x)\;$ could be fulfilled in an empty way, whereas $\;\exists\,x\;P(x)\;$ determines there's at least one such case. $\endgroup$ – Timbuc Oct 16 '14 at 17:34
  • 3
    $\begingroup$ This depends on your rules, but it should go something like the following. Take an arbitrary constant $a$ (assuming the universe is not empty, of course), eliminate $\forall$ with $a$ to get $P(a)$, now introduce $\exists$ to get $\exists xP(x)$. $\endgroup$ – Git Gud Oct 16 '14 at 17:35
  • $\begingroup$ @GitGud But without any further assumptions "like the universe $P$ is not empty" Timbuc and Berci are right, right? $\endgroup$ – displayname Oct 16 '14 at 17:36
  • 2
    $\begingroup$ @StefanFalk Yes, but the universe having at least an object is something that's most likely stated in the first page of the text book, notes, whatever. Something like "from now on there is always at least one constant". $\endgroup$ – Git Gud Oct 16 '14 at 17:38

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)$.


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.


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.