Unary predicate type (${\bigwedge }_{i=1}^k{P}_i(x{)}^{{ϵ}_i}$)

For a fixed finite list of unary predicates, a unary predicate type specifies whether each predicate holds of an element. With $k$ predicates there are $2^k$ possible truth value patterns; a first-order structure may realize any subset of them. The notation $P^1=P$, $P^0=\neg P$ makes each pattern a quantifier-free formula.

The displayed first-order sentence requires a domain with at least $2^k$ elements without using logical equality. Distinct patterns disagree on some predicate, so a single element cannot witness both. Conversely, a domain consisting of the $2^k$ binary strings of length $k$, with $P_i$ selecting strings whose $i$th bit is one, realizes every pattern. More generally, requiring any $m$ distinct unary predicate types forces at least $m$ distinct elements.