Prove by tableau method - Axioms of equality

Question

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?

Answer 1

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).