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


$$ \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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.