= Least representatives of finite equivalence classes
On a finite linearly ordered structure with an equivalence relation, the formula $\forall y(y<x\to\neg E(y,x))$ selects exactly the least element of each equivalence class. Variable-recycling counting therefore expresses any prescribed lower bound on the number of classes. The order and equivalence-relation axioms use three variable names. Finiteness matters: densely interleaved infinite classes need not have least elements.
Back to article page
