# Is Unification "an Implementation of Existential Quantification"?

I read a comment (I've forgotten the source), "Unification is an implementation of existential quantification." (Emphasis mine.)

If true, this point of view clears up many things.

For instance why omitting the "occurs check" in unification can lead to unsound inference: it would be the same as using the assumption of the existence of a thing in your proof(-term) of the existence of that thing.

It would also explain why the algorithms for unification in logic programming language engines I've looked at seem (to me) more arbitrary than other operators such as conjunction and disjunction.

But - is the statement true? Is it an over-simplification?

A more precise statement would be that existential quantification in logic programming languages is (typically) handled by introducing a unification variable. To perform existential introduction, you need to have a term $$t$$. The rule looks like: $$\dfrac{\Gamma\vdash P[t/x]}{\Gamma\vdash\exists x.P}$$
One way to implement this is to just guess a term $$t$$ and then see if we can backchain $$P(t)$$. Of course, for a language like Prolog, there are an infinite number of possible terms, and you have no guidance on what term to guess. A different option is to have $$t$$ be a meta-variable that stands for a term and continue execution on the hope that we can constrain $$t$$ enough to know what to decide later. This is essentially what a unification variable is. Unification itself just constrains what possible terms that meta-variable can be. Then, instead of actually enumerating the (now constrained) terms, we usually return the (simplified) constraints themselves as a compact representation of the set of possible terms, assuming they aren't contradictory (i.e. that that set isn't empty).
Unsurprisingly, the operation unification itself most directly implements is equality. If we did the "exhaustively enumerate terms" approach to handling existential quantification, all the places where we (implicitly) use "unification" could just be straightforward syntactic checks of ground terms. With meta-variables, they instead produce constraints. Of course, this suggests the natural and common generalization of allowing constraints other than syntactic equality, and this leads to constraint logic programming. One generic example of such a constraint is disunification which states what a term (potentially containing meta-variables) cannot be. It is the negation of unification, $$t\not\equiv s$$ states that for all substitutions $$\sigma$$, $$t[\sigma]\neq s[\sigma]$$.