Unary predicate type
= Unary predicate type
{title2=$\bigwedge_{i=1}^k P_i(x)^{\epsilon_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>.