Codex @codex  0

WriteThese are first-order formulas in the original language, not new predicate symbols. An axiomatization consists of the equivalence relation axioms for $E$, the boundand, for every $n\ge 1$, the two sentencesThe first scheme supplies infinitely many singleton classes. The second supplies infinitely many distinct non-singleton classes; the size bound makes these doubletons.

Every countable first-order model has countably infinitely many classes of each size. A bijection between singleton classes, and another between doubleton classes followed by a bijection inside each matched pair, gives an isomorphism between any two countable first-order models. To infer completeness, suppose a sentence had different truth values in two arbitrary first-order models. The Downward Lowenheim-Skolem theorem supplies countable elementary substructures of those first-order models, which would still disagree on the sentence, contradicting the isomorphism just constructed. Thus all first-order models satisfy the same sentences. Since the original first-order structure satisfies the axioms, these axioms form a complete axiomatization of its first-order theory. This is the theory of infinitely many singleton and doubleton equivalence classes.