Ground expression

In mathematical logic, a ground term of a formal system is a term that does not contain any free variables. 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 C {displaystyle C} the set of constant symbols, V {displaystyle V} the set of (individual) variables, F {displaystyle F} the set of functional operators, and P {displaystyle P} the set of predicate symbols. Ground terms are terms that contain no variables. They may be defined by logical recursion (formula-recursion): Roughly speaking, the Herbrand universe is the set of all ground terms. A ground predicate or ground atom or ground literal is an atomic formula all of whose argument terms are ground terms. If p∈P is an n-ary predicate symbol and α1, α2, ..., αn are ground terms, then p(α1, α2, ..., αn) is a ground predicate or ground atom.