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 può essere costruita dall'universo di Herbrand di , applicando a ogni suo elemento qualche predicato di . È dunque l'insieme di tutti gli atomi ground che possono essere costruiti usando simboli da . Prende il nome da Jacques Herbrand. Nella base di Herbrand ogni elemento viene chiamato atomo.

Un'interpretazione su è completa per tutte le clausole di 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 .

Termini e atomi di HerbrandModifica

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

Esempi:  ,  ,  ,  ,  ,...

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

Esempi:  ,  ,  ,  , ...

Universo e base di HerbrandModifica

L'universo di Herbrand è l'insieme di tutti i termini di Herbrand. Esempio:  

La base di Herbrand è l'insieme di tutti gli atomi di Herbrand. Esempio:  

Sistemi di HerbrandModifica

Dato un enunciato universale, della forma   (  non contiene quantificatori), il sistema di Herbrand è l'insieme (anche infinito) di formule chiuse generato per sostituzione   con tutte le possibili combinazioni   di   appartenente a  . Esempi:

 
 

Sistema di Herbrand di una teoriaModifica

Data una teoria   di enunciati universali, il sistema di Herbrand della teoria   è l'unione   di tutti i sistemi di Herbrand generati dagli enunciati  .

Esempio:

 
 

Teorema di HerbrandModifica

Un enunciato universale   è insoddisfacibile se e solo se esiste un sottoinsieme finito di   contraddittorio nel senso della logica proposizonale.

Il teorema di Herbrand è importante in quanto riduce la soddisfacibilità/validità (sono concetti duali, infatti   è soddisfacibile se e solo se   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)Modifica

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

  •   è soddisfacibile.
  •   ha un modello di Herbrand.

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

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