I am stuck on how to progress with this proof; i cannot see my next move.

The task is to show $S \to \exists x Q(x) \vdash \exists x (S \to Q(x))$ using natural deduction for predicate logic.

My first attempt was the following;

1: $S \to \exists x Q(x) \space \space \space \space \space \space premise$
2: $x_{0} \space \space S \to Q(x_{0}) \space \space assumption$ (start of scoped box, i do not know how to write them here)
3: $\exists x(S \to Q(x)) \space \space \exists x \space introduction \space 2$ (end of scoped box)
4: $\exists x(S \to Q(x)) \space \space \exists x \space elimination \space 1,2-3$

However, i am not so sure that this is correct. The rule for $\exists$ elimination is
$\frac{\exists x \phi \space \space(And \space we \space manage \space to \space infer \space \gamma \space from \space replacing \space x \space in \phi \space with \space a \space fresh \space variable)}{\gamma}$
I do not know how to render the rule here (bonus question), but here's a link to where it is better described (page 16).

In order to eliminate $\exists x$ i must thus have a formula $\exists x \phi$ as my premise, and the other premise as described in the link above. However, my first premise in this case is $S \to \exists x Q(x)$, which makes me think my second move is illegal.

Can anyone explain if my thinking is correct, and point out my next move, or if i am wrong please explain why i am wrong? (Incidentally the link above describes exactly those rules my course litterature allow me to use, so if i could get help in terms of those rules i would be doubly grateful).

  • $\begingroup$ You should assume S, then you can ... $\endgroup$ Commented Aug 6, 2018 at 19:44
  • $\begingroup$ @ThomasKlimpel S is not a premise, nor is it derivable from the given premise. The premise only states that if S is true, then so is the consequent. $\endgroup$
    – mcg256
    Commented Aug 6, 2018 at 23:43
  • $\begingroup$ Take a look at cs.uwaterloo.ca/~plragde/cs245old/02-propnd.pdf page 27. In that terminology, you should "introduce a proof box, which is a way of marking the fact that you made the assumption S". Then you can eliminate the implication from you premise, and then eliminate $\exists$. Then you can close the proof box by introducing the implication again, and then ... $\endgroup$ Commented Aug 7, 2018 at 5:06
  • 1
    $\begingroup$ @mcg256 Well, it turns out that my suggestion was not the way to go for this proof. Take a look at 6005's answer (and maybe his last comment before I agreed that his solution is correct). This means that your answer is just as incorrect as my suggestion, sorry. $\endgroup$ Commented Aug 8, 2018 at 7:30
  • $\begingroup$ @ThomasKlimpel Thanks for pointing me there. We were both wrong, but at least someone (@6005) was able to help out! $\endgroup$
    – mcg256
    Commented Aug 13, 2018 at 23:15

2 Answers 2


In order to eliminate $\exists x$ i must thus have a formula $\exists x \phi$ as my premise, and the other premise as described in the link above. However, my first premise in this case is $S \to \exists x Q(x)$, which makes me think my second move is illegal.

Exactly right. Your second move was illegal for the reason you said.

The problem is a bit tricky because of the annoying $S \to$ in front of the $\exists x Q(x)$, which means we can't eliminate the existential just yet. In order to get to $\exists x Q(x)$, we need to first have a proof of $S$, or know that $S$ is true. But we don't!

So how do we remove $S$ in front if we don't know it's true? Try first proving, as a lemma, that $S \lor \lnot S$: the law of the excluded middle. Next, your proof will have two cases: one if $S$ is true, and one if $S$ is not true. If $S$ is true, you should be able to eliminate the existential to get your $x$. If $S$ is not true, you should be able to prove $\exists x (S \to Q(x))$ by taking any $x$ at all.

By the way, in case you're interested: one reason this inference is difficult to solve is that not all logicians agree with it! There are logicians who proposed something called "Free Logic", with the main idea being that it is possible for no objects to exist at all. If no objects exist at all, then $S \to \exists x Q(x)$ might be true (it will be true if $S$ is false), but $\exists x (S \to Q(x))$ is definitely false no matter what, because there does not exist any $x$ period.

  • $\begingroup$ Your answer definitely does not describe a "natural deduction proof", but it is basically right otherwise. The "natural deduction" proof systems allows you to (temporarily) eliminate the annoying implication without assuming the law of excluded middle. The problem with using "natural deduction" in a beginners course is that this system has desirable technical qualities beyond the scope of a beginners course. This makes it hard to explain why things have to be done in the way prescribed by the system. $\endgroup$ Commented Aug 7, 2018 at 8:05
  • $\begingroup$ @ThomasKlimpel I don't agree it doesn't describe a natural deduction proof. "Natural deduction" means different things to different authors -- I have seen a basic variant of the sequent calculus described as natural deduction, but more common is the system where you introduce and discharge premises via introduction and elimination rules. The elimination rule for implication requires that we have $S$ before we can get to $\exists x Q(x)$. Perhaps your natural deduction system is not the one I am using here? $\endgroup$ Commented Aug 7, 2018 at 15:49
  • $\begingroup$ Both "natural deduction" and "sequent calculus" (and also "analytic tableau") have a certain core technical meaning beyond specific representations of the calculus. Your suggestion "Try first proving, as a lemma, the law of the excluded middle" seems to me to be incompatible with that core technical meaning. There are good reasons for authors to use some simpler less strict calculus for an introduction to logic. But even if they would name such a simplified calculus "natural deduction" or "sequent calculus", it would still not change the real meaning of those terms. $\endgroup$ Commented Aug 7, 2018 at 18:18
  • 1
    $\begingroup$ @ThomasKlimpel I think we're on the same page about the definitions: I'm fine with the definition in the notes you linked. I am honestly just trying to figure out why you disagree that this is a valid natural deduction proof. Do you just disagree with the phrase "prove as a lemma"? If so, this should be perfectly compatible with natural deduction. Whether writing the proof out as a tree or as a sequence of lines, you simply deduce $S \lor \lnot S$ from no premises, then prove the conclusion from each of $S$ and $\lnot S$, and finish with $\lor$ elimination. $\endgroup$ Commented Aug 7, 2018 at 23:16
  • 1
    $\begingroup$ OK, now I see. You are right, sorry. Probably I was lead in the wrong direction by my comment "I believe your answer is not strictly wrong, but ..." on mcg256's answer (and your comment on Free Logic, which I used to justify an incorrect step in my "own imagined" proof). $\endgroup$ Commented Aug 8, 2018 at 7:24

I don't believe the Existential elimination in your step two is correct.

On page 16 of your text, the $\phi$ is scoped within the Existential Quantifier expression, and you've tried to eliminate it in the scope of the implication $S \rightarrow \exists x Q(x) $.

I believe you can use a subproof to show $\exists x Q(x) \dashv \vdash Q(x_0)$. I.e. That the two well formed formulas are semantically equivalent. And the proof of each direction is $\exists$ introduction one way, and $\exists$ elimination for the other.

Then you could use that information to conclude $S \rightarrow Q(x_0)$. Since the consequent of the premise's implication is semantically equivalent to it.

From there, you can use $\exists$ introduction, with $\phi=S\rightarrow Q(x_0)$, to conclude $\exists x(S \rightarrow Q(x_0))$, as you've already done.

Hope that helps!

  • $\begingroup$ I believe your answer is not strictly wrong, but it doesn't describe a strict "natural deduction proof" either. But even if we interpret it as describing a "natural deduction proof", the subproof only needs to show $\exists x Q(x) \vdash Q(x_0)$, no need to also show $\exists x Q(x) \dashv Q(x_0)$. $\endgroup$ Commented Aug 7, 2018 at 5:21
  • $\begingroup$ Oops, I upvoted this but I just noticed there's a problem with it. $\exists x Q(x)$ and $Q(x_0)$ are not equivalent. The latter implies the former, but the former does not apply the latter, because even though we know that some $x$ satisfies $Q$, we don't know that $x_0$ satisfies $Q$. Using free variables in lemmas in this way is a bit sketchy in general. $\endgroup$ Commented Aug 7, 2018 at 5:37
  • $\begingroup$ @6005 That's a good point! Is there a way for you to remove your upvote? $\endgroup$
    – mcg256
    Commented Aug 13, 2018 at 23:12
  • $\begingroup$ @mcg256 The upvote locks in place, but if you edit the answer, then the system will let me remove it. Of course, you could edit to just explain the problem, then there will be no need to remove the upvote. $\endgroup$ Commented Aug 13, 2018 at 23:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.