 Unary predicate type

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.