Predicate Logic - Natural Deduction; Assumptions about exists-elimination

Question

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

Answer 1

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.

Answer 2

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!