Composition of relations ($R\circ S=\{(x,z):\exists y,xRy,ySz\}$)

This convention composes paths in their written order; some sources instead reverse that convention. Composition of relations is associative. Taking inverse relations reverses the order: $(R\circ S{)}^{-1}=S^{-1}\circ R^{-1}$.

// Target: foundations-of-mathematics.bigb

If $R\subseteq R^{\prime }$ and $S\subseteq S^{\prime }$, then $R\circ S\subseteq R^{\prime }\circ S^{\prime }$. A witness joining a pair through $R$ and then $S$ also joins it through the larger relations. If both $R$ and $S$ are reflexive relations on the same set, inserting an identity step gives $R\cup S\subseteq R\circ S$, so monotonicity also gives $(R\cup S{)}^2\subseteq (R\circ S{)}^2$.

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.