Theory of pure equality

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.

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.

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.

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

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