Give a Hilbert-style proof $ \vdash ( x=y \rightarrow y = x) $

Question

Give a Hilbert-style proof $$ \vdash ( x=y \rightarrow y = x) $$

---

I don't know where to start. I thought maybe I can use Ax5 (Identity axiom) $ x = x $ as a starting point.

See George Tourlakis, Mathematical Logic (2008) or this post for a list of axioms and theorems.

Answer 1

If you want, you can "rewrite" Amr's proof with Tourlakis' rules as follows.

Start from Ax6 [page 139] : this group contains all formulae of the form :

$\vdash t = s \rightarrow (A[x := t] \equiv A[x :=s])$.

It is called the "Leibniz axiom (group) for equality".

Using the following instance of Ax6, with $A(x) := (w = x)$ :

$\vdash x = y \rightarrow ((w = x)[w := x] \equiv (w = x)[w := y])$

we get :

$\vdash x = y \rightarrow ((x = x) \equiv (y = x))$.

Now, as per Amr's answer, assume :

$x = y$;

by modus ponens we get :

$x = y \vdash ((x = x) \equiv (y = x))$.

But we have Ax5 : $\vdash x = x$; using Equanimity [page 39] we have :

$x = y \vdash y = x$.

A last step with Deduction Theorem and we will have :

$\vdash (x = y \rightarrow y = x).$

Answer 2

I don't which proof system you are using.

$x=y\,\,\,\,\,\,\,\,$ (Given)

Assume $ \lnot(y=x)\,\,\,\,\,\,\, $

Therefore $\lnot(y=y)$ (Let $P(x,y)$ be $\lnot(x=y)$, since we know $x=y$ as a given. We can use Leibniz rule to deduce $P(y,y)$ by substituting $y$ for $x$ to get $\lnot(y=y)$)

$y=y$ (because this is axiom AX5 as you say in your question)

Contradiction

Therefore $\lnot \lnot(y=x)$

Thus, $y=x$

$\square$