title: Espressione ground
text: # Espressione ground
  
  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 $Q(a)\lor P(b)$, con $a$ e $b$ appartenenti all'alfabeto delle costanti, è detta formula ground.
  
  ## Esempi
  
  Prendiamo ad esempio le seguenti espressioni della logica del primo ordine, la cui segnatura contiene i simboli costanti $0$ e $1$ per rappresentare rispettivamente i numeri 0 e 1, il simbolo $s$ per la funzione ad un solo argomento che restituisce il successore del numero in input, e il simbolo $+$ per la funzione di addizione.
  
  * $s(0),s(s(0)),s(s(s(0))),\ldots$ sono termini ground;
  * $0+1,\;0+1+1,\ldots$ sono termini ground;
  * $0+s(0),\;s(0)+s(0),\;s(0)+s(s(0))+0$ sono termini ground;
  * $x+s(1)$ and $s(x)$ sono termini, ma non termini ground;
  * $s(0)=1$ and $0+0=0$ sono formule ground.
  
  ## Definizioni formali
  
  Nelle definizioni seguenti consideriamo un linguaggio del primo ordine in cui $C$ è l'insieme dei simboli costanti, $F$ è l'insieme degli operatori di funzione e $P$ è l'insieme dei predicati.
  
  ### Termine ground
  
  Un termine ground è un termine che non contiene variabili.
  
  I termini ground possono essere definiti ricorsivamente come segue:
  
  * Gli elementi di $C$ sono termini ground;
  * Se $f\in F$ è il simbolo di una funzione $n$-aria e $\alpha _{1},\alpha _{2},\ldots ,\alpha _{n}$ sono termini ground, allora $f\left(\alpha _{1},\alpha _{2},\ldots ,\alpha _{n}\right)$ è un termine ground.
  * 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.
  
  ### Atomo ground
  
  Un atomo ground (o predicato ground) è una formula atomica in cui tutti i termini sono ground.
  
  Se $p\in P$ è il simbolo di un predicato $n$-ario e $\alpha _{1},\alpha _{2},\ldots ,\alpha _{n}$ sono termini ground, allora $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. Invece, l'interpretazione di Herbrand assegna un valore di verità ad ogni atomo ground nella base.
  
  ### Formula ground
  
  Una formula ground è una formula senza variabili.
  
  Le formule senza variabili possono essere definite ricorsivamente come segue:
  
  * Un atomo ground è una formula ground.
  * Se $\varphi$ e $\psi$ sono formule ground, allora $\lnot \varphi$, $\varphi \lor \psi$ e $\varphi \land \psi$ sono formule ground.
  
  Le formule ground sono un particolare tipo di formule chiuse.
  
  