To install click the Add extension button. That's it.

The source code for the WIKI 2 extension is being checked by specialists of the Mozilla Foundation, Google, and Apple. You could also do it yourself at any point in time.

Kelly Slayton
Congratulations on this excellent venture… what a great idea!
Alexander Grigorievskiy
I use WIKI 2 every day and almost forgot how the original Wikipedia looks like.
Live Statistics
English Articles
Improved in 24 Hours
Added in 24 Hours
Show all languages
What we do. Every page goes through several hundred of perfecting techniques; in live mode. Quite the same Wikipedia. Just better.

Ground expression

From Wikipedia, the free encyclopedia

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 and , the sentence is a ground formula. A ground expression is a ground term or ground formula.


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

  • are ground terms;
  • are ground terms;
  • are ground terms;
  • and are terms, but not ground terms;
  • and are ground formulae.

Formal definitions

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

Ground term

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

  1. Elements of are ground terms;
  2. If is an -ary function symbol and are ground terms, then 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, the Herbrand universe is the set of all ground terms.

Ground atom

A ground predicate, ground atom or ground literal is an atomic formula all of whose argument terms are ground terms.

If is an -ary predicate symbol and are ground terms, then is a ground predicate or ground atom.

Roughly speaking, the Herbrand base is the set of all ground atoms,[1] while a Herbrand interpretation assigns a truth value to each ground atom in the base.

Ground formula

A ground formula or ground 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 and are ground formulas, then , , and are ground formulas.

Ground formulas are a particular kind of closed formulas.

See also

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


  1. ^ Alex Sakharov. "Ground Atom". MathWorld. Retrieved October 20, 2022.
This page was last edited on 12 July 2023, at 22:35
Basis of this page is in Wikipedia. Text is available under the CC BY-SA 3.0 Unported License. Non-text media are available under their specified licenses. Wikipedia® is a registered trademark of the Wikimedia Foundation, Inc. WIKI 2 is an independent company and has no affiliation with Wikimedia Foundation.