Satisfaction for a set structure ($\mathrm{Sat}(A,e,\vec{a})$)

The satisfaction relation says that the finite code $e$ of a first-order formula is true in a set-sized first-order structure $A$ at assignment $\vec{a}$. It is defined uniformly in set theory by recursion on the finite syntax tree: evaluate atomic relations, Boolean operations and quantifiers over the given domain. A code includes only finitely many subformulas, and their truth relations are sets. This does not define a truth predicate for the ambient universe, whose domain is not a set. Finite relation closure for set-theoretic coding gives an explicit closure criterion ensuring that these truth relations are computed correctly in a transitive set.