Chiusura universale ed esistenziale

Definizione: Data una formula $\varphi$ con variabili libere $FV(\varphi)=\{x_1,..., x_n\}$

• la chiusura universale di $\varphi$ è la formula chiusa

  $$ U(\varphi)=\forall x_1,...,\forall x_n\varphi $$

• la chiusura esistenziale di $\varphi$ è la formula chiusa

  $$ Ex(\varphi)=\exist x_1,...,\exist x_n \varphi $$

Lemma:

• $\varphi$ è valida se e solo se $U(\varphi)$ è valida
• $\varphi$ è soddisfacibile se e solo se $Ex(\varphi)$ è soddisfacibile

Forme di Skolem

Data una formula $\varphi$, la formula $Ex^S(\varphi)$ — la skolemizzazione della chiusura esistenziale di $\varphi$ — è chiusa e in forma di Skolem, e si ha che:

$$ \varphi \text{ è soddisfacibile }\iff Ex(\varphi)\text{ è soddisfacibile }\iff Ex^S(\varphi)\text{ è soddisfacibile} $$

Quindi, ogni formula è equisoddisfacibile a una formula chiusa in forma di Skolem.

• Esempio

Termini ground

Definizione: Un termine è ground ( o chiuso) se non contiene variabili. Un’istanza ground di un termine $f(t_1,...,t_n)$ è un termine ground ottenuto sostituendo la variabile $x$ con un termine ground del linguaggio:

• sostituendola con il termine ground $c$, si ottiene l’istanza ground $f(c, g(c))$
• sostituendola con il termine ground $f(c, g(c))$, si ottiene un’altra istanza ground $f(f(c, g(c)), g(c))$
• ecc

Universo di Herbrand

Definizione: Sia $\varphi$ una formula chiusa e in forma di Skolem. L’universo di Herbrand $H(\varphi)$ di $\varphi$ è l’insieme dei termini ground costruibili a partir dai simboli di $\varphi$. Se $\varphi$ non contiene simboli di costante, se ne aggiunge uno nuovo, e si costruiscono i termini ground a partire da questo.