View source for Theory of pure equality

{{Short description|Decidable theory of equality}}
In [[mathematical logic]] the '''theory of pure equality''' is a [[first-order logic#First-order theories, models, and elementary classes|first-order theory]]. It has a [[signature (mathematical logic)|signature]] consisting of only the equality relation symbol, and includes no non-logical axioms at all.<ref>{{Cite book| last1=Monk | first1=J. Donald | title=Mathematical Logic | publisher=[[Springer-Verlag]] | location=Berlin, New York | series=Graduate Texts in Mathematics | isbn=978-0-387-90170-1 | year=1976 | url-access=registration | url=https://archive.org/details/mathematicallogi00jdon | page=240 | chapter=Chapter 13: Some Decidable Theories}}</ref>
This theory is [[consistency|consistent]] but incomplete, as a non-empty [[set (mathematics)|set]] with the usual equality relation provides an interpretation making certain sentences true. It is an example of a [[Decidability (logic)|decidable]] theory and is a fragment of more expressive decidable theories, including monadic class of first-order logic (which also admits unary predicates and is, via [[Skolem normal form]], related<ref>{{cite book |last1=Bachmair |first1=L. |last2=Ganzinger |first2=H. |last3=Waldmann |first3=U. |title=&#91;1993&#93; Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science |chapter=Set constraints are the monadic class |date=1993 |pages=75–83 |doi=10.1109/LICS.1993.287598|hdl=11858/00-001M-0000-0014-B322-4 |isbn=0-8186-3140-6 |s2cid=2351050 }}</ref> to [[set constraint]]s in [[program analysis]]) and [[Monadic second-order logic|monadic second-order theory]] of a pure set (which additionally permits quantification over predicates and whose signature extends to monadic second-order logic of ''k'' successors<ref>{{cite journal |last1=Rabin |first1=Michael O. |title=Decidability of Second-Order Theories and Automata on Infinite Trees |journal=Transactions of the American Mathematical Society |date=July 1969 |volume=141 |pages=1–35 |doi=10.2307/1995086|jstor=1995086 |url=http://projecteuclid.org/euclid.bams/1183529958 }}</ref>).
== Historical significance ==
The theory of pure equality was proven to be [[Decidability (logic)|decidable]] by [[Leopold Löwenheim]] in 1915.
If an additional axiom is added saying that there are exactly ''m'' objects for a fixed [[natural number]] ''m'', or an axiom scheme is added saying that there are infinitely many objects, then the resulting theory is [[complete theory|complete]].
== Definition as FOL theory ==
The pure theory of equality contains formulas of [[first-order logic]] with equality, where the only predicate symbol is equality itself and there are no function symbols.
Consequently, the only form of an atomic formula is <math>x=y</math> where <math>x,y</math> are (possibly identical) variables. Syntactically more complex formulas can be built as usual in first-order logic using propositional connectives such as  <math>\land, \lor, \lnot</math> and quantifiers <math>\forall,\exists</math>.
A [[mathematical logic#first-order structures|first-order structure with equality]] interpreting such formulas is just a set with the equality relation on its elements. Isomorphic structures with such signature are thus sets of the same [[cardinality]]. Cardinality thus uniquely determines whether a sentence is true in the structure.
=== Example ===
The following formula:
:<math>
\forall x, y, z.\ (z = x \lor z = y)
</math>
is true when the set interpreting the formula has at most two elements.
== Expressive power ==
{{see|Spectrum of a sentence|Counting quantification}}
This theory can express the fact that the domain of interpretation has at least <math>k</math> elements for a constant <math>k</math> using the formula that we will denote <math>D_k</math> for a constant <math>k</math>:
:<math>
\exists x_1, \ldots, x_k.\ \bigwedge_{1 \le i < j \le k} x_i \ne x_j
</math>
Using negation, it can then express that the domain has more than <math>k</math> elements. More generally, it can constrain the domain to have a given finite set of finite cardinalities.
== Definition of the theory ==
In terms of models, pure theory of equality can be defined as set of those first-order sentences that are true for all (non-empty) sets, regardless of their cardinality. For example, the following is a valid formula in the pure theory of equality:
:<math>
(\forall x, y, z.\ (z = x \lor z = y)) \lor
(\exists p,q,r.\ p \neq q \land p \neq r \land q \neq r)
</math>
By completeness of first-order logic, all valid formulas are provable using axioms of first-order logic and the [[first-order logic#Equality and its axioms|equality axioms]] (see also [[equational logic]]).
== Decidability ==
Decidability can be shown by establishing that every sentence can be shown equivalent to a propositional combination of formulas about the cardinality of the domain.<ref>{{Cite book| last1=Monk | first1=J. Donald | title=Mathematical Logic | publisher=[[Springer-Verlag]] | location=Berlin, New York | series=Graduate Texts in Mathematics | isbn=978-0-387-90170-1 | year=1976 | url-access=registration | url=https://archive.org/details/mathematicallogi00jdon | page=241 | chapter=Chapter 13: Some Decidable Theories, Lemma 13.11}}</ref>
To obtain [[quantifier elimination]], one can expand the signature of the language while preserving the definable relations (a technique that works more generally for monadic second-order formulas). Another approach to establish decidability is to use [[Ehrenfeucht–Fraïssé game]]s.
== See also ==
* [[List of first-order theories]]
* [[Equational logic]]
* [[Free theory]]
== References ==
{{reflist}}
[[Category:Formal theories]]
{{mathlogic-stub}}