How should sequent calculus be extended if we add equality to the first order logic?

Question

Are sequent calculus needed to be extended if we add equality to the first order logic? Is it not enough to say that we just have one more predicate that has all the properties of equality:

$\forall X . \forall Y . [E(X, Y) \implies E(Y, X)]$

$\forall X . \forall Y . \forall Z . [(E(X, Y) \land E(Y, Z)) \implies E(X, Z)]$

If it is not enough, how exactly sequent calculus has to be extended? Or, in other words, what inference rules have to be added?

By the "rules of inference" I mean rules like 12 rules given here in the green box.

Answer 1

No, the rules you've written are not enough.

First, note that what you've written down - symmetry and transitivity - aren't enough to guarantee that $=$ ever holds. You also need reflexivity: that we're allowed to infer, from no hypotheses at all, $t_1=t_1$ for any term $t_1$.

• More precisely, reflexivity is the rule which allows us to infer the sequent $\vdash t_1=t_1$ for any term $t_1$ from no hypotheses whatsoever. On that note, your own rules should be rephrased in sequent calculus language, e.g. from the sequents $\Gamma\vdash t_1=t_2$ and $\Gamma\vdash t_2=t_3$ we can infer the sequent $\Gamma\vdash t_2=t_3$.

More subtly, we need the substitution property, that from $t_1=t_2$ and $\varphi$ we can infer any formula $\psi$ gotten from $\varphi$ by replacing some instances of $t_1$ by $t_2$. After all, equality isn't just any old equivalence relation, it's the finest possible equivalence relation. And this needs to be reflected in the logical rules which govern it.

• Again more precisely: whenever $t_1,t_2$ are terms, $\varphi,\psi$ are formulas, and $\psi$ is gotten from $\varphi$ by replacing some instances of $t_1$ with $t_2$, we have the rule which lets us infer the sequent $\Gamma\vdash\psi$ from the sequents $\Gamma\vdash\varphi$ and $\Gamma\vdash t_1=t_2$.

That this is in fact all we need is a consequence of the relevant completeness theorem (soundness being trivial), and working through the details is a good exercise. Note that the usual (Henkin) proof of (the contrapositive of) completeness should go through unchanged for all reasonable systems: given a consistent theory $T$, we whip up an extension $T'$ in a possibly larger language which is consistent, complete and has the witness property; we then form the term structure for $T'$ and show that it in fact is a model of $T'$ - at which point its reduct to the language of $T$ is a model of $T$, and so $T$ is satisfiable.

---

Finally, note as an aside that reflexivity and substitution on their own give symmetry and transitivity:

• For symmetry, given $t_1=t_2$ we use reflexivity to introduce $t_1=t_1$. Using $t_1=t_2$ as the substituter and $t_1=t_1$ as the substitutee, we get $t_2=t_1$ by changing the first occurrence of $t_1$ to $t_2$ in the substitutee.

• For transitivity, given $t_1=t_2$ and $t_2=t_3$ we use substitution with $t_2=t_3$ as the substituter and $t_1=t_2$ as the substitutee to get $t_1=t_3$.

So reflexivity and substitution are in fact the only equality rules we really need.