Universal formula (source code)

= Universal formula
{title2=$\forall\mathbf y\,\theta(\mathbf x,\mathbf y)$}

A <universal formula> has a block of <universal quantifiers> followed by a <quantifier-free formula>. Empty blocks are usually permitted. Truth transfers from a <first-order structure> to a <substructure of a first-order structure> for parameters in that substructure: every tuple in the smaller domain is available in the larger domain, and quantifier-free truth is preserved and reflected by the inclusion. This is the dual preservation direction to the forward preservation of an <existential formula> under a <structure embedding>.