Ground-term substructure
ID: ground-term-substructure
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.
New to topics? Read the docs here!