{{Short description|Term that does not contain any variables}} {{use dmy dates|date=May 2025}} {{Formal languages}} 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 <math>a</math> and <math>b</math>, the sentence <math>Q(a) \lor P(b)</math> 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 <math>0</math> and <math>1</math> for the numbers 0 and 1, respectively, a unary function symbol <math>s</math> for the successor function and a binary function symbol <math>+</math> for addition. * <math>s(0), s(s(0)), s(s(s(0))), \ldots</math> are ground terms; * <math>0 + 1, \; 0 + 1 + 1, \ldots</math> are ground terms; * <math>0+s(0), \; s(0)+ s(0), \; s(0)+s(s(0))+0</math> are ground terms; * <math>x + s(1)</math> and <math>s(x)</math> are terms, but not ground terms; * <math>s(0) = 1</math> and <math>0 + 0 = 0</math> are ground formulae.
==Formal definitions==
What follows is a formal definition for first-order languages. Let a first-order language be given, with <math>C</math> the set of constant symbols, <math>F</math> the set of functional operators, and <math>P</math> 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 <math>C</math> are ground terms; # If <math>f \in F</math> is an <math>n</math>-ary function symbol and <math>\alpha_1, \alpha_2, \ldots, \alpha_n</math> are ground terms, then <math>f\left(\alpha_1, \alpha_2, \ldots, \alpha_n\right)</math> 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 <math>p \in P</math> is an <math>n</math>-ary predicate symbol and <math>\alpha_1, \alpha_2, \ldots, \alpha_n</math> are ground terms, then <math>p\left(\alpha_1, \alpha_2, \ldots, \alpha_n\right)</math> is a ground predicate or ground atom.
Roughly speaking, the Herbrand base is the set of all ground atoms,<ref>{{MathWorld |id=GroundAtom |title=Ground Atom |author=Alex Sakharov |access-date=2025-05-04 }}</ref> 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 <math>\varphi</math> and <math>\psi</math> are ground formulas, then <math>\lnot \varphi</math>, <math>\varphi \lor \psi</math>, and <math>\varphi \land \psi</math> are ground formulas.
Ground formulas are a particular kind of closed formulas.
==See also==
* {{annotated link|Open formula}} * {{annotated link|Sentence (mathematical logic)}}
== Notes== {{reflist}}
==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}}
{{Mathematical logic}}
Category:Logical expressions Category:Mathematical logic