# In First-Order Logic, can you deduce an existential quantifier purely from other existential quantifiers?

Let's say we have:

∃x(Fx → Gx) and ∃xFx

can we deduce ∃xGx?

I've been throwing myself at this problem for days and every time it just seems like the entire enterprise is flawed.

Existential Elimination seems like the right strategy, yet since we have two different premises, we have to give different instantiations for each one, so no modus ponens. Since we're given different instantiations, there's effectively no way they can ever cross and it seems like we're blindly trying to derive ∃xGx from nothing.

Thinking it through without the symbolization it does seem to make a certain sense (if we know something is F, and we know that if something is F it must be G, it follows that there is some G), yet I just can't find a way to get there without violating the rules of FOL.

Is this problem solvable? If so, what am I missing?

• This becomes a lot easier when you rewrite "$\rightarrow$" as a disjunction: you're trying to deduce $\exists x(G(x))$ from $\exists x(F(x))$ and $\exists x(\neg F(x)\vee G(x))$. That should suggest a strategy for a counterexample ... – Noah Schweber Jul 21 '19 at 3:36

This tree proof generator is able to find a countermodel:

The countermodel considers a domain with two members, {0,1). F is true only when x = 0 and G has no element of the domain that makes it true. Then using x = 1, the conditional, F1 → G1, is true since F1 is false and G1 is also false. Using x=0 for the second premise we have F0 is true. This makes the antecedent true. However, the consequent is false for all values of x. Because a true antecedent yields a false consequent the argument is invalid.

As the OP puts it:

Since we're given different instantiations, there's effectively no way they can ever cross and it seems like we're blindly trying to derive ∃xGx from nothing.

Tree Proof Generator. Retrieved on July 20, 2019 at https://www.umsu.de/logik/trees/

This is not a valid inference. The reason is that one object may satisfy Fx → Gx while another satisfies Fx. There's then no guarantee that anything satisfies Gx.

Here's an example. There is a person A who, whenever he is hungry, eats ice cream. We have: ∃x(Fx → Gx). Person B is hungry. We have: ∃xFx. It doesn't follow that someone eats ice cream.