# Predicate Logic Natural Deduction: $∃x P(x) ⊢P(x)$

I am really puzzled right now.

To solve the issue, I need to prove this formular:

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

with the natural deduction rules for propositional and predicate logic.

I am sure this example should not be that difficult but, yep, now I am here.

For me, it should not be a counter example, so it should be solvable. I started to use exists elimination to get rid of the $$\exists$$, but than I end up with something like this:

\begin{align} \exists x P(x) \vdash P(x) \\ 1.&\ \exists x P(x) \ \text{(prem)} \\ 2.&\ P(x_0) \ \text{(x_0 fresh/free)} \\ 3.&\ \dots (get \ x \ instead \ of \ x_0)\\ 4.&\ P(x) \end{align}

So I miss the little hint how I can transform the new variable to the existing one.

I hope someone can guide me.

Thank you.

• How are your rules defined? There are many systems of natural deduction, each with their own rules. And, given that $\vdash$ means: 'can be derived using the rules of the system we're working with', we'd need to know those rules before we can help you. – Bram28 Dec 30 '18 at 14:17
• This should not be possible to derive. If, for example, we're working in $\mathbb N$ and $P(x)$ is $x=0$, then $\exists x(x=0)$ is true, but $x=0$ is not in general true -- and you shouldn't be able to derive anything but truths when you start with truths. – Henning Makholm Dec 30 '18 at 14:24
• – whati001 Dec 30 '18 at 14:27
• @whati001 As Henning says, the statement you're trying to prove is false. – Alex Kruckman Dec 30 '18 at 17:48
• It might be a good idea to backtrack to the problem you were trying to solve before setting your heart on proving the false claim presented above. – hardmath Dec 30 '18 at 18:15

As suggested by Henning Makholm's comment, $$\exists x P(x) \vdash P(x)$$ is not provable. If it were provable then you could take a derivation of $$\exists x P(x) \vdash P(x)$$ and, by applying the rule $$\forall_I$$ in your list for natural deduction, you would get a derivation of $$\exists x P(x) \vdash \forall x P(x)$$, which is not provable. Indeed, $$\exists x P(x) \vdash \forall x P(x)$$ means that if there exists something with the property $$P$$ then everything has the property $$P$$, which is clearly falsifiable: take $$\mathbb{N}$$ as domain, and let $$P(x)$$ be the property "$$x$$ is even", so that in this structure $$\exists x P(x)$$ is true but $$\forall x P(x)$$ is false.