Ground expression

In mathematical logic, a ground term of a formal system is a term that does not contain any free variables.

Similarly, a ground formula is a formula that does not contain any free variables. In first-order logic with identity, the sentence ${\displaystyle \forall }$ x (x=x) is a ground formula.

A ground expression is a ground term or ground formula.

Consider the following expressions from first order logic over a signature containing a constant symbol 0 for the number 0, a unary function symbol s for the successor function and a binary function symbol + for addition.

What follows is a formal definition for first-order languages. Let a first-order language be given, with ${\displaystyle C}$ the set of constant symbols, ${\displaystyle V}$ the set of (individual) variables, ${\displaystyle F}$ the set of functional operators, and ${\displaystyle P}$ the set of predicate symbols.

...
Wikipedia