How do you prove ∃x[Fx → (Gx → Hx)], ∀xFx ∧ ∃xGx ∴ ∃x¬(Gx ∧ ¬Hx) in FOL?

Question

Given:

∃x[Fx → (Gx → Hx)]

∀xFx ∧ ∃xGx

Prove:

∃x¬(Gx ∧ ¬Hx)

Answer 1

Starting off:

∃x[Fx → (Gx → Hx)]
∀xFx ∧ ∃xGx

We know that F is true for all x (because ∀xFx), so we can replace Fx with true in the first statement.

∃x[true → (Gx → Hx)]

We know that A → B is short for ¬A V B, so we can do that here:

∃x[¬(true) V (Gx → Hx)]
∃x[false V (Gx → Hx)]

We know that false or X is equal to X:

∃x[false V (Gx → Hx)]
∃x[(Gx → Hx)]

And we can apply the definition of implies (→) again:

∃x[(Gx → Hx)]
∃x[¬Gx V Hx]

And finally we can use De Morgan's law ((A V B) <=> ¬(¬A ∧ ¬B)) to invert the contents of the brackets, and simplify not-nots:

∃x[¬Gx V Hx]
∃x[¬(¬(¬Gx) ∧ ¬(Hx))]
∃x[¬(¬¬Gx ∧ ¬Hx)]
∃x[¬(Gx ∧ ¬Hx)]
∃x¬[Gx ∧ ¬Hx]

Which is what you wanted to prove.