Logic proofs using Tableau method (symmetry of a predicate)

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.

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.
• Depending on the proof system, either you'll have to convert your negated $\forall$'s to (not negated) $\exists$'s before substituting constants, or there will be a separate rule for negated $\forall$'s. In any case, the proof system won't allow you to use the same $c$ for both variables. Apr 30 '20 at 1:46
• If you use the three equation I gave above: 1. ∀x∀y∀z(¬x=y∧p(z,x)∧p(z,y)→s(x,y)), 2. ∀x∀y(s(x,y)→¬x=y∧∃z(p(z,x)∧p(z,y))), and 3. ¬(∀x∀y(s(x,y)↔s(y,x))), plus the equation 4. $\forall x \neg p(x,x)$, you should be able to close all branches of the tree. So what I think is that if you define the s(x,y) predicate from p(x,y) or you have to define s(x,y) assuming the necessary axioms for that matter. I am not sure if what I'm saying makes sense, but I think it is true you can prove the symmetry in the first way. Apr 30 '20 at 23:19