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 , con e 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 e per rappresentare rispettivamente i numeri 0 e 1, il simbolo per la funzione ad un solo argomento che restituisce il successore del numero in input, e il simbolo per la funzione di addizione. sono termini ground; sono termini ground; sono termini ground; and sono termini, ma non termini ground; and sono formule ground.
Definizioni formali Nelle definizioni seguenti consideriamo un linguaggio del primo ordine in cui è l'insieme dei simboli costanti, è l'insieme degli operatori di funzione e è 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 sono termini ground; Se è il simbolo di una funzione -aria e sono termini ground, allora è 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 è il simbolo di un predicato -ario e sono termini ground, allora è 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 e sono formule ground, allora , e sono formule ground.
Le formule ground sono un particolare tipo di formule chiuse.
Note
Bibliografia
Voci correlate Formula aperta Formula chiusa
Collegamenti esterni
Logica matematica