CS205: Building with Artificial Intelligence

There are several different conventions for using equality (or identity) in first-order logic. The most common convention, known as first-order logic with equality, includes the equality symbol as a primitive logical symbol which is always interpreted as the real equality relation between members of the domain of discourse, such that the "two" given members are the same member. This approach also adds certain axioms about equality to the deductive system employed. These equality axioms are:

• Reflexivity. For each variable $x, x = x$.
• Substitution for functions. For all variables x and y, and any function symbol $f$,
• $x = y → f(..., x, ...) = f(..., y, ...)$.
• Substitution for formulas. For any variables x and y and any formula φ(x), if φ' is obtained by replacing any number of free occurrences of x in φ with y, such that these remain free occurrences of y, then:

These are axiom schemas, each of which specifies an infinite set of axioms. The third schema is known as Leibniz's law, "the principle of substitutivity", "the indiscernibility of identicals", or "the replacement property". The second schema, involving the function symbol f, is (equivalent to) a special case of the third schema, using the formula:

$x = y → (f(..., x, ...) = z → f(..., y, ...) = z)$.

Many other properties of equality are consequences of the axioms above, for example:

• Symmetry. If $x = y$ then $y = x$.
• Transitivity. If $x = y$ and $y = z$ then $x = z.$

First-order logic without equality

An alternate approach considers the equality relation to be a non-logical symbol. This convention is known as first-order logic without equality. If an equality relation is included in the signature, the axioms of equality must now be added to the theories under consideration, if desired, instead of being considered rules of logic. The main difference between this method and first-order logic with equality is that an interpretation may now interpret two distinct individuals as "equal" (although, by Leibniz's law, these will satisfy exactly the same formulas under any interpretation). That is, the equality relation may now be interpreted by an arbitrary equivalence relation on the domain of discourse that is congruent with respect to the functions and relations of the interpretation.

When this second convention is followed, the term normal model is used to refer to an interpretation where no distinct individuals a and b satisfy $a = b$. In first-order logic with equality, only normal models are considered, and so there is no term for a model other than a normal model. When first-order logic without equality is studied, it is necessary to amend the statements of results such as the Löwenheim–Skolem theorem so that only normal models are considered.

First-order logic without equality is often employed in the context of second-order arithmetic and other higher-order theories of arithmetic, where the equality relation between sets of natural numbers is usually omitted.

Defining equality within a theory

If a theory has a binary formula $A(x,y)$ which satisfies reflexivity and Leibniz's law, the theory is said to have equality, or to be a theory with equality. The theory may not have all instances of the above schemas as axioms, but rather as derivable theorems. For example, in theories with no function symbols and a finite number of relations, it is possible to define equality in terms of the relations, by defining the two terms s and t to be equal if any relation is unchanged by changing $s$ to t in any argument.

Some theories allow other ad hoc definitions of equality:

• In the theory of partial orders with one relation symbol ≤, one could define $s = t$ to be an abbreviation for $s ≤ t ∧ t ≤ s$.
• In set theory with one relation ∈, one may define $s = t$ to be an abbreviation for $∀x (s ∈ x ↔ t ∈ x) ∧ ∀x (x ∈ s ↔ x ∈ t)$. This definition of equality then automatically satisfies the axioms for equality. In this case, one should replace the usual axiom of extensionality, which can be stated as $\forall x\forall y[\forall z(z\in x\Leftrightarrow z\in y)\Rightarrow x=y]$, with an alternative formulation $\forall x\forall y[\forall z(z\in x\Leftrightarrow z\in y)\Rightarrow \forall z(x\in z\Leftrightarrow y\in z)]$, which says that if sets x and y have the same elements, then they also belong to the same sets.