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.

  • $\begingroup$ 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. $\endgroup$ – Bram28 Dec 30 '18 at 14:17
  • 7
    $\begingroup$ 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. $\endgroup$ – Henning Makholm Dec 30 '18 at 14:24
  • $\begingroup$ Rules: teaching.iaik.tugraz.at/_media/lub/deduction.pdf $\endgroup$ – whati001 Dec 30 '18 at 14:27
  • $\begingroup$ @whati001 As Henning says, the statement you're trying to prove is false. $\endgroup$ – Alex Kruckman Dec 30 '18 at 17:48
  • 2
    $\begingroup$ 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. $\endgroup$ – 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.

Said differently, there is no way to fill the dots in your attempt of derivation, using natural deduction inference rules.


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.