Universal sentences are preserved by substructures (source code)

= Universal sentences are preserved by substructures

Quantifier-free <logical formulas> have the same <truth value> in a <substructure> and its ambient <first-order structure> on <tuples> from the smaller carrier. <First-order term> evaluation agrees; atomic relations agree by restriction; Boolean connectives preserve agreement. A universally quantified quantifier-free matrix true on all ambient <tuples> is therefore true on all <substructure> <tuples>.