Base di Herbrand

In logica matematica, per ogni linguaggio formale con un insieme di termini dall'universo di Herbrand, la base di Herbrand definisce ricorsivamente l'insieme di tutte le formule atomiche che possono essere composte formando predicati dai termini dell'universo di Herbrand. Una base di Herbrand di un linguaggio del primo ordine $L$ può essere costruita dall'universo di Herbrand di $L$, applicando a ogni suo elemento qualche predicato di $L$. È dunque l'insieme di tutti gli atomi ground che possono essere costruiti usando simboli da $L$. Prende il nome da Jacques Herbrand. Nella base di Herbrand ogni elemento viene chiamato atomo.

Un'interpretazione su $H(S)$ è completa per tutte le clausole di $S$ quando a ogni atomo della base si assegna un valore di verità.

La base di Herband è un insieme numerabile, i cui elementi possono essere ordinati. Per esempio, possono essere disposti in una successione ordinata $\{P1,P2,\ldots ,Pn\}$.

Termini e atomi di Herbrand

Dato un linguaggio $L(po)$, un termine di Herbrand è un termine base (ground term, ossia un termine che non contiene variabili)

Esempi: $f(a)$, $g(a,b)$, $g(f(a),b)$, $g(f(a),g(b,c))$, $g(f(a),g(f(b),c))$,...

Un atomo di Herbrand è un atomo base (ground atom, ossia un atomo che non contiene variabili)

Esempi: $P(f(a))$, $P(g(a,b))$, $Q(g(f(a),b)$, $g(f(a),g(b,c)))$, ...

Universo e base di Herbrand

L'universo di Herbrand è l'insieme di tutti i termini di Herbrand. Esempio: $U(H)=\{a,b,c,f(a),g(a,b),g(f(a),b),g(f(a),g(b,c)),g(f(a),g(f(b),c)),\dots \}$

La base di Herbrand è l'insieme di tutti gli atomi di Herbrand. Esempio: $B(H)=\{P(a),P(b),P(c),P(f(a)),P(g(a,b)),Q(g(f(a),b),g(f(a),g(b,c))),\dots \}.$

Sistemi di Herbrand

Dato un enunciato universale, della forma $\forall x_{1}\forall x_{2}\dots \forall x_{n}\varphi$ ($\varphi$ non contiene quantificatori), il sistema di Herbrand è l'insieme (anche infinito) di formule chiuse generato per sostituzione $\varphi [x_{1}/t_{1},x_{2}/t_{2},\dots ,x_{n}/t_{n}]$ con tutte le possibili combinazioni $<t_{1},t_{2},\ldots ,t_{n}>$ di $t(i)$ appartenente a $U(H)$. Esempi:

$H(\forall xP(x)\in Q(x)))=\{P(f(a))\in Q(f(a)),P(g(a,b))\in Q(g(a,b)),\ldots \}$

$H(\forall x\forall yR(x,y))=\{R(f(a),f(a)),R(g(a,b),f(a)),R(f(a),g(a,b)),\ldots \}.$

Sistema di Herbrand di una teoria

Data una teoria $\Sigma$ di enunciati universali, il sistema di Herbrand della teoria $\Sigma$ è l'unione $H(\Sigma )$ di tutti i sistemi di Herbrand generati dagli enunciati $\Sigma$.

Esempio:

$\Sigma =\{\varphi ,\psi ,X\}$

$H\left(\Sigma \right)=H(\varphi )\bigcup H(\psi )\bigcup H(X).$

Teorema di Herbrand

Un enunciato universale $\forall x_{1}\cdots \forall x_{n}\ \varphi$ è insoddisfacibile se e solo se esiste un sottoinsieme finito di $H(\varphi )$ contraddittorio nel senso della logica proposizonale.

Il teorema di Herbrand è importante in quanto riduce la soddisfacibilità/validità (sono concetti duali, infatti $\varphi$ è soddisfacibile se e solo se $\neg \varphi$ non è logicamente valida) della logica predicativa del primo ordine alla logica proposizionale, in quanto per ogni formula esiste una formula universale equisoddisfacibile (skolemizzazione). Esso fornisce anche un metodo di semi-decisione (e non di decisione, in quanto l'Entscheidungsproblem è indecidibile) per testare la soddisfacibili/validità di una formula della logica predicativa del primo ordine.

Corollario (forma a clausole di Horn)

Sia $\tau$ un insieme di clausole di Horn, le seguenti affermazioni sono equivalenti:

• $\tau$ è soddisfacibile.
• $\tau$ ha un modello di Herbrand.

È da notare che si afferma che $\tau$ ha un modello di Herbrand, non $H(\tau )$. Non vale in generale: solo se $\tau$ è un insieme clausole di Horn. In questa forma (finita), è quasi una procedura effettiva.

Collegamenti esterni

• (EN) Eric W. Weisstein, Base di Herbrand, su MathWorld, Wolfram Research.