= Satisfaction for a set structure
{title2=$\operatorname{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>.
Back to article page
