### 12.7.2 Unique Names Assumption

Instead of being agnostic about the equality of each term and expecting the user to axiomatize which names denote the same individual and which denote different individuals, it is often easier to have the convention that different ground terms denote different individuals.

**Example 12.43:**Consider a student database example where a student must have two courses as science electives. Suppose a student has passed

*math302*and

*psyc303*; then you only know whether they have passed two courses if you know

*math302≠psyc303*. That is, the constants

*math302*and

*psyc303*denote different courses. Thus, you must know which course numbers denote different courses. Rather than writing

*n×(n-1)*inequality axioms for

*n*individuals, it may be better to have the convention that every course number denotes a different course and thus the use of inequality axioms is avoided.

This approach to handling equality is known as the unique names assumption.

The **unique names assumption (UNA)** is
the assumption that distinct ground terms denote different
individuals. That is, for every pair of distinct ground
terms *t _{1}* and

*t*, assume

_{2}*t*, where "

_{1}≠t_{2}*≠*" means "not equal to."

Note that this does not follow from
the semantics for the definite clause language.
As far as that semantics was concerned, distinct ground terms
*t _{1}* and

*t*could denote the same individual or could denote different individuals.

_{2}In the logic presented thus far, the unique names assumption only matters if explicit inequalities exist in the bodies of clauses or equality in the head of clauses. With the unique names assumption, equality does not appear in the head of clauses, other than in the clauses defining equality presented earlier. Other clauses implying equality would be either tautologies or inconsistent with the unique name axioms.

The unique names assumption can be axiomatized with the following axiom schema for inequality, which consists of the axiom schema for equality together with the axiom schema:

*c≠c'*for any distinct constants*c*and*c'*.*f(X*for any distinct function symbols_{1},...,X_{n})≠g(Y_{1},...,Y_{m})*f*and*g*.*f(X*, for any function symbol_{1},...,X_{n})≠f(Y_{1},...,Y_{n})←X_{i}≠Y_{i}*f*. There are*n*instances of this schema for every*n*-ary function symbol*f*(one for each*i*such that*1 ≤ i ≤ n*).*f(X*for any function symbol_{1},...,X_{n})≠c*f*and constant*c*.*t≠X*for any term*t*in which*X*appears (where*t*is not the term*X*).

With this axiomatization, two ground terms are not equal if and only
if they do not unify, because ground terms are identical if and only if they
unify. This is not the case for non-ground terms. For example, *a≠X* has some instances that are *true* - for example, when *X* has value *b*
- and an instance which is *false*, namely, when *X* has value *a*.

The unique names assumption is very useful for database applications,
in which you do not, for example, want to have to state that *kim≠sam* and *kim≠chris* and *chris≠sam*. The
unique names assumption allows us to use the convention that each
name denotes a different individual.

Sometimes the unique names assumption is inappropriate - for example, *2+2 ≠4* is wrong, nor may it be the case that *clark_kent≠superman*.