I need to construct a semantic tree in order to check the validity of this formula:
$$(\exists y)(\exists x)P(x, y) \leftrightarrow (\exists x)(\forall y)P(x,y)$$
I denoted the left part of the formula with $A$ and the right part with $B$. Now, here's what I've got:
A <-> B
/ \
A ~A
B ~B
$\sim A$ becomes $(\forall y)(\forall x) \sim P(x, y)$ and $\sim B$ becomes $(\forall x)(\exists y) \sim P(x, y)$.
This is where I got stuck because I don't know how I should proceed. Thank you in advance!
Well, it's a good thing that you didn't go any further with that first tree, because if you want to check the validity of that formula, then your tree should start with the negation of that formula!
Why?
Well, if you take the formula as is, and you find the tree closes, then it is clearly not a valid formula ... but if the tree does not close, then that does not mean that the formula is valid, for all that that would mean is that it is possible for the formula to be true, not that it is necessarily true.
On the other hand, if you start the tree with the negation of the formula, and find the tree closes, then we know the negation of the formula cannot possibly be true, meaning that the original formula cannot possibly be false, and hence is valid. And if that tree leads to an open branch, then we know the negation of the formula can be true, meaning that the original formula can be false, and hence is not valid.
OK, so in your second attempt you set things up correctly but there are still some issues:
The right side is correct!
On the left side: Yes, you instantiated the universal with $a$ and $b$, but you obtained $c$ and $d$, and so now you need to instantiate that universal with them! ... and now you see the problem: everytime you instantiate that universal with a newly obtained constant, you get a new existential, and that existential gets you a new constant, so now you need to instantiate the uiversal with that one, etc. etc. .... you get what is called an infinite tree ... and so you can never get to the point where you can say the branch is open and finished!
Thankfully, there is a solution to this ... though I don't know if your book has defined the existential rule this way ...:
When dealing with an existential, you should really create a branch for every constant already appearing in the branch with the existential and in that branch you use that particular constant to instantiate the existential with. Do this for every constant you have, but also create one more branch where you do use a new constant. That way, you explore the possibility of possibly satisfying an existential with an earlier defined constant, and if that works, you can actually obtain an open and finished branch. If it doesn't work, well, you still have that one other branch with a new constant that you can work with.
So: After you instantiate the first existential on the left with an $a$, create two branches to deal with the $\exists y Pay$: in one branch you put $Paa$, and in the second you put $Pab$. Now deal with the $\forall x \exists y \ \neg Pxy$, making sure that in each of the two branches you instantiate that univeral with each of the constants that appear in that branch, i.e. in the one branch you instantiate it with just $a$, and in the other with both $a$ and $b$ (that'll basically be like the branch as you have it now) ... but now you get another existential to deal with ... so branch for that one as well.
OK, try that!