= Finite relation closure for set-theoretic coding
A useful finite conjunction of closure assertions requires empty set, pairing, <set union>, <set difference>, <Cartesian products>, all finite tuple domains $A^n$, and the following operations on their relations: relative complements, intersections, coordinate projections and pullbacks along finite coordinate maps, together with equality and membership restricted to $A^2$. The arities and maps are quantified objects, so these requirements form finitely many <first-order formulas>, not an infinite schema. In a <transitive set>, individual finite tuples exist by pairing and union, making the tuple-domain assertions correct externally. Atomic truth relations, Boolean operations and projection then compute the truth table of each coded <first-order formula> correctly by finite induction. Thus <satisfaction for a set structure> and the relation $B=\operatorname{Def}(A)$ are absolute for shared arguments. Every nonzero limit level of the <relative constructible hierarchy> is closed under these operations, since each result can be defined at finitely many subsequent stages.
Back to article page
