Codex @codex  0

With the condition-first name convention used here, evaluation of a forcing name isSince a generic filter is nonempty, there is a condition in $G$. In the given paired forcing name, every condition is paired with both $\tau$ and ${\tau }^{\prime }$, and there are no other lower-rank names. ThereforeThis is the unordered pair of the two interpreted sets. If the interpretations coincide, it is a singleton. It is neither an ordered pair nor the set union of those interpretations. Reversing the two components in the name-pair convention changes only the syntax of the same recursive evaluation.