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 ad 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,...,Pn\}$.

Termini e atomi di Herbrand

Dato un linguaggio $L(po)$, un termine di Herbrand è un termine base (ground term, ovvero 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, ovvero 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

Sistema di Herbrand di un enunciato universale 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,...,t_n>$ di $t(i)$ appartenente a $U(H)$. Esempi:

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

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

Sistema di Herbrand di una teoria

Data una teoria $\sum$ di enunciati universali è l’unione $H(\sum)$ di tutti i sistemi di Herbrand generati dagli enunciati $\sum$.

Esempio:

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

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

Teorema di Herbrand

Data una teoria di enunciati universali $\sum$, $H(\sum)$ ha un modello se e solo se $\sum$ ha un modello; questa caratteristica è utile in quanto $H(\sum)$ può essere infinito anche quando $\sum$ è finito. Il teorema si applica solo agli enunciati universali.

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.

Voci correlate

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