Ground expression

Ground expression

In mathematical logic, a ground term of a formal system is a term that does not contain any variables at all, and a closed term is a term that has no free variables. In first-order logic all closed terms are ground terms, but in lambda calculus the closed term λ x. xy. y) is not a ground term.

Similarly, a ground formula is a formula that does not contain any variables, and a closed formula or sentence is a formula that has no free variables. In first-order logic with identity, the sentence \forall x (x=x) is not a ground formula.

A ground expression is a ground term or ground formula.

Contents

Examples

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.

  • s(0), s(s(0)), s(s(s(0))) ... are ground terms;
  • 0+1, 0+1+1, ... 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;
  • s(z)=1 and ∀x: (s(x)+1=s(s(x))) are expressions, but are not ground expressions.

Ground expressions are necessarily closed. The last example, ∀x: (s(x)+1=s(s(x))), shows that a closed expression is not necessarily a ground expression. So, this formula is a closed formula, but not a ground formula, because it contains a logical variable, even though that variable is not free.

Formal definition

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

Ground terms

Ground terms are terms that contain no variables. They may be defined by logical recursion (formula-recursion):

  1. elements of C are ground terms;
  2. If fF is an n-ary function symbol and α1, α2 , ..., αn are ground terms, then f1, α2 , ..., αn) 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 or ground atom is an atomic formula all of whose terms are ground terms. That is,

If pP is an n-ary predicate symbol and α1, α2 , ..., αn are ground terms, then p1, α2 , ..., αn) is a ground predicate or ground atom.

Roughly speaking, the Herbrand base is the set of all ground atoms, 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 all of whose arguments are ground atoms.

Ground formulae may be defined by syntactic recursion as follows:

  1. A ground atom is a ground formula; that is, if pP is an n-ary predicate symbol and α1, α2 , ..., αn are ground terms, then p1, α2 , ..., αn) is a ground formula (and is a ground atom);
  2. If p and q are ground formulae, then ¬(p), (p)∨(q), (p)∧(q), (p)→(q), formulas composed with logical connectives, are ground formulae, too.
  3. If p is a ground formula and we can get q from it that way some ( or ) we delete or insert in the p formula, and then the result, q is well-formed and equivalent with p, then q is a ground formula.[clarification needed]
  4. We can get all ground formulae applying these three rules.

References


Wikimedia Foundation. 2010.

Игры ⚽ Нужна курсовая?

Look at other dictionaries:

  • Ground Zero — Pour les articles homonymes?, voir Ground zero (homonymie). Ground zero est un terme anglais utilisé pour indiquer l endroit précis sur le sol où a lieu n importe quelle explosion …   Wikipédia en Français

  • ground — ground, grounds Both the singular and the plural are used in the expressions on the ground (or grounds) that, and grounds is more common in the expression grounds for (complaint etc.): • Occupations that various insurance companies consider to be …   Modern English usage

  • ground swell — noun 1. an obvious change of public opinion or political sentiment that occurs without leadership or overt expression there was a ground swell of antiwar sentiment • Hypernyms: ↑transition 2. a broad and deep undulation of the ocean • Syn: ↑heavy …   Useful english dictionary

  • expression — /Ik spreSFn/ noun 1 WORDS (C) a word or group of words with a particular meaning: The expression in the family way means pregnant . | pardon/forgive/excuse the expression (=used when you have used a word that you think may offend someone): He… …   Longman dictionary of contemporary English

  • expression —    by Claire Colebrook    Expression is one of Deleuze s most intense concepts. If we take Deleuze s definition of a concept that it is a philosophical creation that produces an intensive set of ordinates then expression can be understood as… …   The Deleuze dictionary

  • expression —    by Claire Colebrook    Expression is one of Deleuze s most intense concepts. If we take Deleuze s definition of a concept that it is a philosophical creation that produces an intensive set of ordinates then expression can be understood as… …   The Deleuze dictionary

  • Ground reaction force — In classical mechanics the term ground reaction force (GRF) refers generically to any force exerted by the ground on a body in contact with it. [cite web last = first = authorlink = coauthors = title = Definition of ground reaction force work =… …   Wikipedia

  • Ground zero — Pour les articles homonymes, voir Ground zero (homonymie). Article détaillé : Site du World Trade Center. Ground zero (point zéro) est un terme anglais utilisé pour indiquer l endroit précis sur le sol où a lieu n importe quelle explosion …   Wikipédia en Français

  • ground rent lease — An expression familiar in Maryland but anomalous in some other jurisdictions. The chief characteristics of the Maryland ground rent leases are (1) the owner of the land in fee leases it to the named lessee for the period of ninety nine years, (2) …   Ballentine's law dictionary

  • Freedom of expression in India — Indians belive in value of Satyam Shivam Sundaram Truth is God and God is beautiful [http://www.youtube.com/watch?v=MClteDdwtvM Prayer on you tube] .Satyameva Jayate is India’s national motto. The English translation of the Sanskrit Satyameva… …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”