Editing First-order logic (section)

===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 [[definitional extension|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 order]]s with one relation symbol ≤, one could define ''s'' = ''t'' to be an abbreviation for ''s'' ≤ ''t'' {{and}} ''t'' ≤ ''s''.
* In set theory with one relation ∈, one may define ''s'' = ''t'' to be an abbreviation for {{math|∀''x'' (''s'' ∈ ''x'' ↔ ''t'' ∈ ''x'') {{and}} ∀''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 <math>\forall x \forall y [ \forall z (z \in x \Leftrightarrow z \in y) \Rightarrow x = y]</math>, with an alternative formulation <math>\forall x \forall y [ \forall z (z \in x \Leftrightarrow z \in y) \Rightarrow \forall z (x \in z \Leftrightarrow y \in z) ]</math>, which says that if sets ''x'' and ''y'' have the same elements, then they also belong to the same sets.