I do not quite understand yet how the proof of a formula works in first order logic. I am currently having the following problem that I assume it is due to lack of comprehension.
The problem is as follows, if I want to proof that a predicate is symmetric. Let us suppose we are talking about s(x,y) defined as "x has a sibling y". I may define this in terms of p(x,y) "x is the parent of y" (let's assume for simplicity that the parent is unique) by the formulae:
$$\forall x \forall y \forall z\, (\neg x = y \wedge p(z,x) \wedge p(z,y) \rightarrow s(x,y)),$$ $$\forall x \forall y\, (s(x,y)\rightarrow \neg x = y \wedge \exists z (p(z,x) \wedge p(z,y))).$$
Here's the thing. If I aim to proof s(x,y) is symmetric, this is,
$$\forall x\forall y\, (s(x,y)\leftrightarrow s(y,x)),$$ and I use the tableau to do so, I should consider $$\neg(\forall x\forall y\, (s(x,y)\leftrightarrow s(y,x))).$$ Then, I introduce the new constant $c$ and obtain
(additional question, there are two $\forall$ and in both cases I am replacing its values for the new constant $c$. Is this correct whenever I consider the $\forall$ constant introduction? Even when I know the predicate should be false when considering s(x,x))
which gives rise to a closed branch. But this would mean all predicates of two "variables" are symmetric and, for instance, $p(x,y)$ is not.
I'm afraid my main problem is to understand what I am doing. So, I would like to understand the what is going on here. May I assume I know s(x,y) is symmetric because we know the relation having a sibling is? Does it change (conceptually) if I define this predicate using the p(x,y) predicate? I would love to read some lines on this topic to clarify these questions/misconceptions.
Thank you in advance.