# Unification-based elimination rule for equality

A few years back, I ran across the following left-rule for equality in sequent calculus:

$$\frac{s \doteq t \leadsto \theta \qquad \theta(\Gamma) \vdash \theta(C)} {\Gamma, s \doteq t \vdash C}$$

Here, $s \doteq t \leadsto \theta$ computes the most general unifier $\theta$ for $s$ and $t$, and then applies the substition to the conclusion $C$ and all the hypotheses in the context $\Gamma$.

The interesting thing about this unification is that it equates finds a substitution for universal (i.e., skolem) variables.

However, I cannot remember where I read this, and was wondering if anyone could help me find a reference to it.

I've often attributed this to Rules of definitional reflection by Schroeder-Heister, though the idea goes back beyond that to Girard and others; the rule you're looking for is an instance of the first display in Section 4. You also, however, need a rule that says that if the unification instance is unsatisfiable, then the assumption of equality has the force of a contradiction.

A more general account has been used recently in a lot of work by Dale Miller, David Baelde, and company (see, for instance, Least and greatest fixed points in linear logic). The more general formulation - which also doesn't originate with Miller et al - is that the rule is

$${\{\theta \in {\sf csu}(t,s) \mid \theta\Gamma \vdash \theta{C} \}}\over{\Gamma, t \doteq s \vdash C}$$

where ${\sf csu}(t,s)$ is the complete set of unifiers - the set of all unifying substitutions of $t$ and $s$. You might also prefer the equivalent way of writing this rule that I prefer (see here for example).

$${\forall \theta. \theta{t} = \theta{s} \longrightarrow \theta\Gamma \vdash \theta{C}}\over{\Gamma, t \doteq s \vdash C}$$

In any case, in a term language with decidable unification where the existence of a unifier implies the existence of a most general unifier, having either of these rules above can be shown to be equivalent to having these two rules:

$${{{\sf no~mgu}(t,s)}\over{\Gamma, t \doteq s \vdash C}} \qquad {{{\sf mgu}(t,s) = \theta \quad \theta\Gamma \vdash \theta{C}}\over{\Gamma, t \doteq s \vdash C}}$$

(P.S. Frank discussed this in his logic programming course in lectures 6, 7, and 8, which may be where you remember it from.)

• Thanks! I was looking at the wrong papers of Schroeder-Heister. – Neel Krishnaswami May 4 '12 at 14:27