Validity of three quantifier sentences using truth tree

Question

I am having a lot of trouble figuring out how to close the paths of the Truth tree for the following argument:

∀x∀y∀z(Axy->Azx) Conclusion: (∃x∃yAxy ->∀x∀yAxy)

My attempt is as follows:

(1) ∀x∀y∀z(Axy->Azx)

(2) -(∃x∃yAxy ->∀x∀yAxy)

(3) ∃x∃yAxy (from line 2)

(4)-(∀x∀yAxy) (from line 2)

(5) ∃x-∀yAxy (Negative Quantifiers line 4)

(6) -∀yAay (Existential Instantiation (with a) line 5)

(7) ∃yAby (EI (with b) from line 3)

(8) Abc (EI (with c) from line 7)

From here on, I am not sure what to do:

• I don't understand how to deal with the negative quantifier in line 6, as well as how to 'selectively apply Universal Instantiation' to line 1, as well as the order in which to do this.

Any help would be appreciated. Thanks.

Answer 1

Hint

Lines (3) and (4) are managed in the same way:

we have to instantiate them with fresh parameters.

Thus, form them we get respectively:

(3') $Aab$

(4') $\lnot Acd$.

---

Now, having introduced four parameters: $a, b, c, d$, we have to "instantiate" (1) with all possible combinations.

In fact, we need only two:

(5) $Aab \to Aca$ --- with $(a,b,d)$ for $(x,y,z)$.

Now we apply the rule for $\to$ and we have to branches:

($6_L$) $\lnot Aab$ --- this branch will close with (3')

($6_R$) $Ada$.

The second needed instantiation of (1) is:

(7) $Ada \to Acd$ --- with $(d,a,c)$ for $(x,y,z)$.

Now we apply the rule for $\to$ and we have again to branches:

($7_L$) $\lnot Ada$ --- this branch will close with ($6_R$)

($7_R$) $Acd$ --- this branch will close with (4').