Editing First-order logic (section)

==Equality and its axioms==
{{See also|Equality (mathematics)#In logic}}
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:<ref>[[Melvin Fitting|Fitting, M.]], ''First-Order Logic and Automated Theorem Proving'' (Berlin/Heidelberg: Springer, 1990), [https://books.google.com/books?id=eaXbBwAAQBAJ&lpg=PP1&hl=cs&pg=PA198&redir_esc=y#v=onepage&q&f=false pp. 198–200].</ref>{{rp|198–200}}
* ''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 φ(''z'') with a free variable z, then:
*:''x'' = ''y'' → (φ(x) → φ(y)).

These are [[axiom schema]]s, each of which specifies an infinite set of axioms. The third schema is known as ''[[Identity of indiscernibles#Indiscernibility of identicals|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: 
:φ(z): ''f''(..., ''x'', ...) = ''f''(..., ''z'', ...)
Then
:''x'' = ''y'' → (''f''(..., ''x'', ...) = ''f''(..., ''x'', ...) → ''f''(..., ''x'', ...) = ''f''(..., ''y'', ...)).

Since ''x'' = ''y'' is given, and ''f''(..., ''x'', ...) = ''f''(..., ''x'', ...) true by reflexivity, we have ''f''(..., ''x'', ...) = ''f''(..., ''y'', ...)

Many other properties of equality are consequences of the axioms above, for example:
* ''Symmetry''. If ''x'' = ''y'' then ''y'' = ''x''.<ref>Use formula substitution with φ(z) being ''z''=''x'', so, φ(x) is x=x which implies φ(y): y=x, then use reflexivity.</ref>
* ''Transitivity''. If ''x'' = ''y'' and ''y'' = ''z'' then ''x'' = ''z''.<ref>Use formula substitution with φ(a) being ''a''=''z'' to obtain ''y''=''x'' → (''y''=''z'' → ''x''=''z''), then use symmetry and [[uncurrying]].</ref>

===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 [[congruence relation|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 [[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.