In logica matematica, un'espressione ground di un sistema formale è tale per cui i suoi termini non contengono variabili.

Ad esempio, nel contesto della logica del primo ordine, la formula ${\displaystyle Q(a)\lor P(b)}$, con ${\displaystyle a}$ e ${\displaystyle b}$ appartenenti all'alfabeto delle costanti, è detta formula ground.

Prendiamo ad esempio le seguenti espressioni della logica del primo ordine, la cui segnatura contiene i simboli costanti ${\displaystyle 0}$ e ${\displaystyle 1}$ per rappresentare rispettivamente i numeri 0 e 1, il simbolo ${\displaystyle s}$ per la funzione ad un solo argomento che restituisce il successore del numero in input, e il simbolo ${\displaystyle +}$ per la funzione di addizione.

• ${\displaystyle s(0),s(s(0)),s(s(s(0))),\ldots }$ sono termini ground;
• ${\displaystyle 0+1,\;0+1+1,\ldots }$ sono termini ground;
• ${\displaystyle 0+s(0),\;s(0)+s(0),\;s(0)+s(s(0))+0}$ sono termini ground;
• ${\displaystyle x+s(1)}$ and ${\displaystyle s(x)}$ sono termini, ma non termini ground;
• ${\displaystyle s(0)=1}$ and ${\displaystyle 0+0=0}$ sono formule ground.

Nelle definizioni seguenti consideriamo un linguaggio del primo ordine in cui ${\displaystyle C}$ è l'insieme dei simboli costanti, ${\displaystyle F}$ è l'insieme degli operatori di funzione e ${\displaystyle P}$ è l'insieme dei predicati.

Un termine ground è un termine che non contiene variabili.

I termini ground possono essere definiti ricorsivamente come segue:

1. Gli elementi di ${\displaystyle C}$ sono termini ground;
2. Se ${\displaystyle f\in F}$ è il simbolo di una funzione ${\displaystyle n}$-aria e ${\displaystyle \alpha _{1},\alpha _{2},\ldots ,\alpha _{n}}$ sono termini ground, allora ${\displaystyle f\left(\alpha _{1},\alpha _{2},\ldots ,\alpha _{n}\right)}$ è un termine ground.
3. Ogni termine ground può essere generato applicando le due regole di cui sopra.

In altre parole, l'universo di Herbrand è l'insieme di tutti i termini ground.

Un atomo ground (o predicato ground) è una formula atomica in cui tutti i termini sono ground.

Se ${\displaystyle p\in P}$ è il simbolo di un predicato ${\displaystyle n}$-ario e ${\displaystyle \alpha _{1},\alpha _{2},\ldots ,\alpha _{n}}$ sono termini ground, allora ${\displaystyle p\left(\alpha _{1},\alpha _{2},\ldots ,\alpha _{n}\right)}$ è un atomo ground.

In altre parole, la base di Herbrand è l'insieme di tutti gli atomi ground.^[1] Invece, l'interpretazione di Herbrand assegna un valore di verità ad ogni atomo ground nella base.

Una formula ground è una formula senza variabili.

Le formule senza variabili possono essere definite ricorsivamente come segue:

1. Un atomo ground è una formula ground.
2. Se ${\displaystyle \varphi }$ e ${\displaystyle \psi }$ sono formule ground, allora ${\displaystyle \lnot \varphi }$, ${\displaystyle \varphi \lor \psi }$ e ${\displaystyle \varphi \land \psi }$ sono formule ground.

Le formule ground sono un particolare tipo di formule chiuse.

• (EN) M. Dalal, Logic-based computer programming paradigms, in K.H. Rosen e J.G. Michaels (a cura di), Handbook of discrete and combinatorial mathematics, 2000, p. 68.
• (EN) Wilfrid Hodges, A shorter model theory, Cambridge University Press, 1997, ISBN 978-0-521-58713-6.

• Formula aperta
• Formula chiusa

• (EN) First-Order Logic: Syntax and Semantics (PDF), su web.engr.oregonstate.edu.

Portale Matematica: accedi alle voci di Wikipedia che trattano di matematica