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?