# Reflexivity of equality in sequent calculus

In definition 1.3.1 of Johnstone's Sketches of an Elephant are given axioms and rules for first order logic. I recall the ones I need for the question:

(a) The structural rules consist of the identity axiom

$$(\phi \vdash_{\vec x} \phi),$$

the substitution rule

$$\begin{array}{cc} (\phi \vdash_{\vec x} \psi)\\ \hline (\phi[\vec s/ \vec x] \vdash_{\vec y} \psi[\vec s / \vec x]) \end{array}$$

where $\vec y$ is a string of variable including all the variables occurring in the string of terms $\vec s$, and the cut rule

$$\begin{array}{cc} (\phi \vdash_{\vec x} \psi)\ (\psi \vdash_{\vec x} \chi)\\ \hline (\phi \vdash_{\vec x} \chi)) \end{array}$$

(b) The equality rules consist of the axioms

$$\bigl(\top \vdash_{\vec x} (x = x)\bigr)$$

and

$$\bigl((\vec x = \vec y \wedge \phi) \vdash_{\vec z} \phi[\vec y/\vec x]\bigr)$$

where $\vec x$ and $\vec y$ are contexts of the same length and type, $(\vec x = \vec y)$ is a shorthand for $\bigl((x_1 =y_1) \wedge \dots \wedge(x_n = y_n)\bigr)$ and $\vec z$ is any context containing $\vec x, \vec y$ and $\text{FV}(\phi)$.

(c) The rules for (finite) conjunction are the axioms

$$(\phi \vdash_{\vec x} \top), \quad ((\phi_1 \wedge \phi_2 \vdash_{\vec x} \phi_i)\quad (i=1, 2)$$

and the rule

$$\begin{array}{cc} (\phi \vdash_{\vec x} \psi)\ (\phi \vdash_{\vec x} \chi)\\ \hline (\phi \vdash_{\vec x} \psi \wedge \chi) \end{array}$$

It is said it is a standard exercise to derive the sequents

$$\bigl((x = y) \vdash_{x, y} (y=x)\bigr), \quad \bigl((x=y)\wedge (y=z) \vdash_{x, y, z} (x = z)\bigr)$$

and I can derive the second from the first, but I'm not able to derive the first one. I was told that actually the second equality axiom should rather be

$$\bigl((\vec x = \vec y \wedge \phi[\vec x / \vec u]) \vdash_{\vec z} \phi[\vec y/\vec u]\bigr)$$

Is the latter one the right axiom and/or can it be derived? How to derive the simmetry axiom for equality?

From a categorical point of view (using completeness) it is trivial to see that they hold, but I would prefer a proof using sequent calculus.

First, let's derive the transitivity axiom. Taking $\phi$ to be the formula $y = z$, the second equality axiom yields $$x = y \land y = z \vdash x = z$$ as required. On the other hand, taking $\phi$ to be $z = y$, we have $$x = y \land z = y \vdash z = x$$ and applying the substitution $z \mapsto y$, we have $$x = y \land y = y \vdash y = x$$ but $y = y$ is an axiom, so we have the symmetry axiom $$x = y \vdash y = x$$ as required.