= Finite-domain composition from relation predicates
{title2=$(S\circ R)(x,z)\iff\exists y\in Y:\ R(x,y)\land S(y,z)$}
If $R:X\times Y\to\{false,true\}$ and $S:Y\times Z\to\{false,true\}$ expose only membership predicates, composition requires finding whether some middle value satisfies both. A complete finite enumeration of $Y$ makes the query decidable by scanning until a witness is found or all values fail. Without an enumeration or equivalent access operation, generic membership oracles do not supply enough information: a finite query transcript can agree with an all-false case yet omit a fresh middle witness that makes composition true. Known finiteness is not the same as an available traversal. A separate carrier argument preserves the variance of the base predicate interfaces.
Back to article page
