Quantifier-free type

The quantifier-free type of a tuple records all atomic and negated atomic formulas it satisfies, equivalently all quantifier-free formulas. Equal such types identify the generated substructures by sending each term value at one tuple to the value of the same term at the other tuple. Equality formulas make this correspondence well defined, and the relational formulas make it an isomorphism.

In the constant-free language with multiplication as its sole nonlogical symbol, every term in one free variable is $x^k$ for some $k\ge 1$. Every atomic formula $x^r=x^s$ holds at both zero and one. Hence every quantifier-free formula, being a finite Boolean combination of those atoms, has the same truth value at both points. They have the same quantifier-free type, and neither singleton is quantifier-free definable. Quantifiers distinguish them: $\forall y(xy=x)$ defines zero, while $\forall y(xy=y)$ defines one. These formulas do not rely on named zero or one constants.