How does unify predicate (=)/2 differ from first order equality?

Question

The tag logical purity mentions (=)/2 as pure. Is it "intrinsically" pure or "operational" pure? To the best of my knowledge it can be defined by this Horn clause:

∀x(=(x, x))

Which is this Prolog fact, if were not already a built-in:

X = X.

This means (=)/2 would be "intrinsically" pure, as SWI-Prolog already remarks. So what is then the difference to first order equality (FOL=), if there are any differences?

Answer 1

The "intrinsinc" definition of (=)/2 I guess does assure that the unify predicate is reflexive, symmetric and transitive. Requirements that are also satisfied by FOL=. But FOL= also requires congruence, which is this axiom schema:

/* Predicate Congruence in FOL= */

∀x1..∀xn∀yj(=(xj, yj) & p(x1, .., xn) -> p(x1, .., xj-1, yj, xj+1, .., xn))

Which is not represented by the only Horn clause for the unify predicate. And since the unify predicate is a built-in, the missing Horn clauses can also not be added. So what can go wrong? Can we make an example that would go wrong?

The classical example is this fact:

p(morning_star).

Obviously this query succeeds in Prolog:

?- p(morning_star).
true

But this query fails in Prolog, whereas in FOL= it would succeed:

?- morning_star = evening_star, p(evening_star).
false

The situation is different in so called unification modulo theories, where the unification and also the unify predicate might change their meaning.