Show that {∃x(F x & Gx),∀x(Gx → ∼H x)} ⊢ ∃x(x = x & (F x & ∼H x)).

Question

I'm having difficulty with the following question.

For the next few problems, establish the fact in question by producing refutations and then citing the soundness theorem. You may use your intuitions to decide when a finite set of quantifier free sentences is unsatisfiable.

Show that {∃x(Fx & Gx),∀x(Gx → ∼H x)} ⊢ ∃x(x = x & (Fx & ∼Hx)).

I'm not quite sure where to start with this.

Converting it into plain English I got the following...

'There exists some x, such that x = x and F applied to x and the negation of H applied to x'

is provable from

'There exists some x, such that F applied to x and G applied to x, and for all x G applied to x implies the negation of H applied to x'

I'm not sure how to use the soundness theorem or refutation can someone give me some direction please?

Answer 1

1) $∃x(Fx \land Gx)$ --- premise

2) $∀x(Gx → \lnot Hx)$ --- premise

3) $\forall x(x = x)$ --- FOL axiom for equality

4) $Fa \land Ga$ --- assumed [a] from 1) by Existential Elimination, with $a$ new

5) $Ga$ --- from 4)

6) $Fa$ --- from 4)

7) $Ga → \lnot Ha$ --- from 2) by Universal Elimination

8) $\lnot Ha$ --- from 5) and 7) by Modus Ponens

9) $Fa \land \lnot Ha$ --- from 6) and 8)

10) $a=a$ --- from 3) by UE

11) $a=a \land (Fa \land \lnot Ha)$ --- from 10) and 11)

12) $\exists x \ [x=x \land (Fx \land \lnot Hx)]$ --- from 11) by Existential Introduction

The conclusion follows by EE from 4) and 12) and 1), discharging assumption [a].

---

Simple "intuitve check" :

1st premise : "there is someone that is a Philosopher and Greek";

2nd premise : "every Greek is not Irish".

Therefore : "there is someone that is Philosopher and not Irish".