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
$$s(c,c)\leftrightarrow s(c,c),$$
(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.
Ordinarily, the rule for introducing new constants deals with just a single quantifier, so to replace both $x$ and $y$ you'd need to apply the rule twice. Furthermore, the rule says that the constant you introduce has to be new, i.e., not already involved in your proof. So when you replace the second variable by a constant, it can't be the same constant that you used for the first variable. So your error occurs at the point where $s(c,c)$ appeared.