Ground-term substructure (source code)

= Ground-term substructure
{title2=$\langle\varnothing\rangle^{\mathcal A}=\{t^{\mathcal A}:t\text{ closed}\}$}

The values of all <closed terms> in a <first-order structure> form a <substructure> when the <first-order language> has at least one constant. The constant ensures nonemptiness, and applying a <function symbol> to closed-term values again gives a closed-term value. Relations are restricted from the ambient <first-order structure>. Every <universal sentence> true in the ambient <first-order structure> remains true in this <substructure>.