Theory of pure equality

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]).

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.

Syntactically more complex formulas can be built as usual in first-order logic using propositional connectives such as

Cardinality thus uniquely determines whether a sentence is true in the structure.

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.

[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).