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 ${\displaystyle Q(a)\lor P(b)}$, con ${\displaystyle a}$ e ${\displaystyle 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 ${\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.

Definizioni formali

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.

Termine ground

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.

Atomo 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.

Formula ground

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.

Note

1. (EN) Eric W. Weisstein, Ground Atom, in MathWorld, Wolfram Research. URL consultato il 20 ottobre 2022.

Bibliografia

• (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.

Voci correlate

• Formula aperta
• Formula chiusa

Collegamenti esterni

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