Prove by tableau method - Axioms of equality Example:
Let $T^*$ be a theory with axioms of equality. Prove by tableau method that
(a) $T^* \vDash x=y \rightarrow y=x \qquad $  (symmetry of =)
(b) $T^* \vDash (x=y \, \land \,y=z) \rightarrow x=z \qquad$ (transitivity of =)
Hint: To show (a) apply the axiom of equality (iii) for $x_1=x,\; x_2=x,\; y_1=y,\;  y_2=x$, to show (b) apply (iii) for $x_1=x,\; x_2=y,\; y_1=z$
(a) Should the root of the tableau looks like this?

Then I use substitution and I get $F(y_1=x_1) -T(y_1=x_1)-\circ$
Then it is proved right?
 A: You have to use both equality axioms :

$\forall x \ (x=x)$ --- reflexivity
$\forall x \ \forall y \ (x=y) \to (\phi \to \phi')$ --- where $\phi'$ is obtained from $\phi$ by replacing $x$ in zero or more places by $y$ : replacement axiom.

Specifically, the instance of the replacement axiom needed is :


$\forall x \ \forall y \ ((x=y) \to [ (x=x) \to (y=x)])$.



The tableau must start with the axioms and the negation of the conclusion :

$\text F \ [ \ \forall x \ \forall y \ ((x=y) \to (y=x)) ]$.

Thus, you have first to "unpack" the leading quantifiers, correctly using $y_1$ and $x_1$ new, to get:

$\text F \ ((x_1=y_1) \to (y_1=x_1))$

and then :

$\text T \ (x_1=y_1)$
$\text F \ (y_1=x_1)$.

But this does not close.

1) $\text T \ \forall x \ (x=x)$ --- axiom
2) $\text T \ \forall x \ \forall y \ ((x=y) \to [ (x=x) \to (y=x)])$ --- axiom
3) $\text F \ \forall x \ \forall y \ ((x=y) \to (y=x))$ - negation of conclusion
4) $\text T \ (x_1=y_1)$ --- from 3)
5) $\text F \ (y_1=x_1)$ --- from 3)
6) $\text T \ (x_1=x_1)$ --- from 1)
7) $\text T \ ((x_1=y_1) \to [ (x_1=x_1) \to (y_1=x_1)])$ --- from 2).
Left branch:
8)  $\text F \ (x_1=y_1)$ --- closes with 4).
Right branch :
9) $\text T \ ((x_1=x_1) \to (y_1=x_1))$.
Left branch :
10) $\text F \ (x_1=x_1)$ --- closes with 6).
Right branch :
11) $\text T \ (y_1=x_1)$ --- closes with 5).
