Theory of pure equality

In mathematical logic the theory of pure equality is a first-order theory. It has a signature consisting of only the equality relation symbol, and includes no non-logical axioms at all. ^[1]

This theory is consistent but incomplete, as a non-empty set with the usual equality relation provides an interpretation making certain sentences true. It is an example of a 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 ^[2] to set constraints in program analysis) and 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 ^[3] ).

Historical significance

The theory of pure equality was proven to be 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.

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 ${\displaystyle x=y}$ where ${\displaystyle x,y}$ are (possibly identical) variables. Syntactically more complex formulas can be built as usual in first-order logic using propositional connectives such as ${\displaystyle \land ,\lor ,\lnot }$ and quantifiers ${\displaystyle \forall ,\exists }$.

A 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:

${\displaystyle \forall x,y,z.\ (z=x\lor z=y)}$

is true when the set interpreting the formula has at most two elements.

Expressive power

Further information: Spectrum of a sentence and Counting quantification

This theory can express the fact that the domain of interpretation has at least ${\displaystyle k}$ elements for a constant ${\displaystyle k}$ using the formula that we will denote ${\displaystyle D_{k}}$ for a constant ${\displaystyle k}$:

${\displaystyle \exists x_{1},\ldots ,x_{k}.\ \bigwedge _{1\leq i<j\leq k}x_{i}\neq x_{j}}$

Using negation, it can then express that the domain has more than ${\displaystyle k}$ 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:

${\displaystyle (\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)}$

By completeness of first-order logic, all valid formulas are provable using axioms of first-order logic and the 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. ^[4]

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é games.

See also

• List of first-order theories
• Equational logic
• Free theory

References

1. Monk, J. Donald (1976). "Chapter 13: Some Decidable Theories". Mathematical Logic . Graduate Texts in Mathematics. Berlin, New York: Springer-Verlag. p. 240. ISBN   978-0-387-90170-1.
2. Bachmair, L.; Ganzinger, H.; Waldmann, U. (1993). "Set constraints are the monadic class". [1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science. pp. 75–83. doi:10.1109/LICS.1993.287598. hdl:11858/00-001M-0000-0014-B322-4. ISBN   0-8186-3140-6. S2CID   2351050.
3. Rabin, Michael O. (July 1969). "Decidability of Second-Order Theories and Automata on Infinite Trees". Transactions of the American Mathematical Society. 141: 1–35. doi:10.2307/1995086. JSTOR   1995086.
4. Monk, J. Donald (1976). "Chapter 13: Some Decidable Theories, Lemma 13.11". Mathematical Logic . Graduate Texts in Mathematics. Berlin, New York: Springer-Verlag. p. 241. ISBN   978-0-387-90170-1.