Inmathematical logic, aground term of aformal system is aterm that does not contain anyvariables. Similarly, aground formula is aformula that does not contain any variables.

Infirst-order logic with identity with constant symbols${\displaystyle a}$ and${\displaystyle b}$, thesentence${\displaystyle Q(a)\vee P(b)}$ is a ground formula. Aground expression is a ground term or ground formula.

Consider the following expressions infirst order logic over asignature containing the constant symbols${\displaystyle 0}$ and${\displaystyle 1}$ for the numbers 0 and 1, respectively, a unary function symbol${\displaystyle s}$ for the successor function and a binary function symbol${\displaystyle +}$ for addition.

• ${\displaystyle s(0),s(s(0)),s(s(s(0))),\dots }$ are ground terms;
• ${\displaystyle 0+1,0+1+1,\dots }$ are ground terms;
• ${\displaystyle 0+s(0),s(0)+s(0),s(0)+s(s(0))+0}$ are ground terms;
• ${\displaystyle x+s(1)}$ and${\displaystyle s(x)}$ are terms, but not ground terms;
• ${\displaystyle s(0)=1}$ and${\displaystyle 0+0=0}$ are ground formulae.

What follows is a formal definition forfirst-order languages. Let a first-order language be given, with${\displaystyle C}$ the set of constant symbols,${\displaystyle F}$ the set of functional operators, and${\displaystyle P}$ the set ofpredicate symbols.

Aground term is aterm that contains no variables. Ground terms may be defined by logical recursion (formula-recursion):

1. Elements of${\displaystyle C}$ are ground terms;
2. If${\displaystyle f\in F}$ is an${\displaystyle n}$-ary function symbol and${\displaystyle {\alpha }_1,{\alpha }_2,\dots ,{\alpha }_n}$ are ground terms, then${\displaystyle f\left({\alpha }_1,{\alpha }_2,\dots ,{\alpha }_n\right)}$ is a ground term.
3. Every ground term can be given by a finite application of the above two rules (there are no other ground terms; in particular, predicates cannot be ground terms).

Roughly speaking, theHerbrand universe is the set of all ground terms.

Aground predicate,ground atom orground literal is anatomic formula all of whose argument terms are ground terms.

If${\displaystyle p\in P}$ is an${\displaystyle n}$-ary predicate symbol and${\displaystyle {\alpha }_1,{\alpha }_2,\dots ,{\alpha }_n}$ are ground terms, then${\displaystyle p\left({\alpha }_1,{\alpha }_2,\dots ,{\alpha }_n\right)}$ is a ground predicate or ground atom.

Roughly speaking, theHerbrand base is the set of all ground atoms,^[1] while aHerbrand interpretation assigns atruth value to each ground atom in the base.

Aground formula orground clause is a formula without variables.

Ground formulas may be defined by syntactic recursion as follows:

1. A ground atom is a ground formula.
2. If${\displaystyle \phi }$ and${\displaystyle \psi }$ are ground formulas, then${\displaystyle \mathrm{\neg }\phi }$,${\displaystyle \phi \vee \psi }$, and${\displaystyle \phi \wedge \psi }$ are ground formulas.

Ground formulas are a particular kind ofclosed formulas.

• Open formula – Formula that contains at least one free variable
• Sentence (mathematical logic) – In mathematical logic, a well-formed formula with no free variables

• Dalal, M. (2000), "Logic-based computer programming paradigms", in Rosen, K.H.; Michaels, J.G. (eds.),Handbook of discrete and combinatorial mathematics, p. 68
• Hodges, Wilfrid (1997),A shorter model theory,Cambridge University Press,ISBN 978-0-521-58713-6
• First-Order Logic: Syntax and Semantics

• Logical expressions
• Mathematical logic

• Articles with short description
• Short description is different from Wikidata
• Pages that use a deprecated format of the math tags