Truth trees in predicate logic

Question

I am learning about using truth trees to prove validity in predicate logic.

I have learnt about simplifying single existential quantifiers but I have come across this one in the lecture notes that uses 2 existential quantifiers. In such cases how do I begin with the truth tree?

Use a truth tree to determine whether the following is valid: $\exists$x (Fx $\iff$ Gx) $\models$ ($\exists$x Fx $\iff$ $\exists$xGx)

Answer 1

We have to enter the truth tree for the premise, i.e. $∃x(Fx⟺Gx)$, and the negation of the conclusion, i.e. $\lnot (∃xFx ⟺ ∃xGx)$.

Applying the $∃$-rule to the premise we get:

$Fa⟺Ga$, with $a$ new.

The negation of the conclusion is the negation of a bi-conditional.

Thus, we need to branches; the first with: $∃x Fx$ and $\lnot ∃xGx$, and the second one with: $\lnot ∃x Fx$ and $∃xGx$.

Then, we go on with the two branches.

---

Consider the left one:

1) $Fa⟺Ga$

2) $∃x Fx$

3) $\lnot ∃xGx$

4) $\lnot Ga$ --- from 3)

5) $Fb$ --- from 2): $b$ new.

Now we have to unpack 1), producing two branches:

$6_L$) $Fa$

$7_L$) $Ga$

that close: 4)+$7_L$).

And:

$6_R$) $\lnot Fa$

$7_R$) $\lnot Ga$

that does not close.

We may easily check that an interpretation $I$ with $F^I = \{ a \}$ and $G^I = \{ \ \}$ does satisfy the premise but does not satisfy the conclusion.