Prove that the relation $\approx$ over the terms of $\mathcal{L}$ is transitive.

Question

The relation $\approx$ is defined over the set of terms of $\mathcal{L}$ by setting $t \approx t'$ iff $\Gamma \vdash t \doteq t'$.

I am asked to prove that the relation is transitive, using the following two axioms of predicate logic:

AX1- $\forall x\varphi \supset \varphi[t/x]$, if $t$ is free for $x$ in $\varphi$.

AX5- $x\doteq y \supset (\varphi[x/z] \supset \varphi[y/z])$, if both $x$ and $y$ are free for z in $\varphi$.

---

I'm given the case for symmetry, which works out nicely for substituting $x$ for $t$ and $y$ for $t'$. However, I'm not seeing what to do in this case, specifically, what formula I should choose for $\varphi[y/z]$ such that I can can conclude with $t\approx t'$.

Can anyone give me a push?

Answer 1

Hint

It seems to me that you need also the axiom : $x=x$.

In addition, you need modus ponens and the other axioms for predicate calculus, in order to prove at least Deduction Theorem and Generalization Theorem.

---

Having said that, you can apply Ax5 with $z=w$ as $\varphi$ to derive :

(*) $\ \vdash x=y \to (x=w \to y=w)$.

For symmetry, again with Ax5, using $z=x$ as $\varphi$, we get :

$\vdash x=y \to (x=x \to y=x)$;

thus, with $\vdash x=x$, we derive :

$x=y \vdash y=x$,

and conclude with : $\vdash x= y \to y=x$ by Ded Th.

Now we can prove transitivity :

1) $x=y \land y=z$ --- premise

2) $\vdash x = y \to y=x$

3) $y=x$ --- from 1) and 2)

4) $\vdash y=x \to (y=z \to x=z)$ --- by (*) above

5) $x=y \land y=z \vdash x=z$ --- from 1), 3) and 4) by modus ponens

(**) $\vdash x=y \land y=z \to x=z$ --- by Ded Th.

---

Consider now transitivity; assuming : $t \approx t'$ and $t' \approx t''$, i.e.

$\Gamma \vdash t=t'$ and $\Gamma \vdash t'=t''$.

From (**) by Generalization, we get : $\forall x \forall y \forall z \ (x=y \land y=z \to x=z)$.

With Ax1 and modus ponens we derive :

$t=t' \land t'=t'' \to t=t''$;

thus, from the assumptions above we conclude with :

$\Gamma \vdash t=t''$,

i.e. $t \approx t''$.