Ground expression#Ground atom

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

In first-order logic with identity with constant symbols $a$ and $b$ , the sentence $Q(a) \lor P(b)$ is a ground formula. A ground expression is a ground term or ground formula.

Examples

Consider the following expressions in first order logic over a signature containing the constant symbols $0$ and $1$ for the numbers 0 and 1, respectively, a unary function symbol $s$ for the successor function and a binary function symbol $+$ for addition.

$s(0), s(s(0)), s(s(s(0))), \ldots$ are ground terms;
$0 + 1, \; 0 + 1 + 1, \ldots$ are ground terms;
$0+s(0), \; s(0)+ s(0), \; s(0)+s(s(0))+0$ are ground terms;
$x + s(1)$ and $s(x)$ are terms, but not ground terms;
$s(0) = 1$ and $0 + 0 = 0$ are ground formulae.

Formal definitions

What follows is a formal definition for first-order languages. Let a first-order language be given, with $C$ the set of constant symbols, $F$ the set of functional operators, and $P$ the set of predicate symbols.

=Ground term=

A {{visible anchor|ground term}} is a term that contains no variables. Ground terms may be defined by logical recursion (formula-recursion):

Elements of $C$ are ground terms;
If $f \in F$ is an $n$ -ary function symbol and $\alpha_1, \alpha_2, \ldots, \alpha_n$ are ground terms, then $f\left(\alpha_1, \alpha_2, \ldots, \alpha_n\right)$ is a ground term.
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, the Herbrand universe is the set of all ground terms.

=Ground atom=

A {{visible anchor|ground predicate}}, {{visible anchor|ground atom}} or {{visible anchor|ground literal}} is an atomic formula all of whose argument terms are ground terms.

If $p \in P$ is an $n$ -ary predicate symbol and $\alpha_1, \alpha_2, \ldots, \alpha_n$ are ground terms, then $p\left(\alpha_1, \alpha_2, \ldots, \alpha_n\right)$ is a ground predicate or ground atom.

Roughly speaking, the Herbrand base is the set of all ground atoms,{{MathWorld |id=GroundAtom |title=Ground Atom |author=Alex Sakharov |access-date=2025-05-04 }} while a Herbrand interpretation assigns a truth value to each ground atom in the base.

=Ground formula=

A {{visible anchor|ground formula}} or {{visible anchor|ground clause}} is a formula without variables.

Ground formulas may be defined by syntactic recursion as follows:

A ground atom is a ground formula.
If $\varphi$ and $\psi$ are ground formulas, then $\lnot \varphi$ , $\varphi \lor \psi$ , and $\varphi \land \psi$ are ground formulas.

Ground formulas are a particular kind of closed formulas.

Notes

References

{{Cite book | title=Handbook of discrete and combinatorial mathematics | contribution = Logic-based computer programming paradigms | year=2000 | editor1-last = Rosen | editor1-first = K.H. | editor2-last = Michaels | editor2-first = J.G. | last = Dalal | first = M. | page=68}}
{{Cite web|last= Fern|first=Alan|date=2010-01-08|url=https://web.engr.oregonstate.edu/~afern/classes/cs532/notes/fo-ss.pdf|title=Lecture Notes {{!}} First-Order Logic: Syntax and Semantics}}
{{Cite book | last=Hodges | first=Wilfrid | author-link=Wilfrid Hodges | title=A shorter model theory | publisher=Cambridge University Press | isbn=978-0-521-58713-6 | year=1997}}

Category:Logical expressions

Category:Mathematical logic