Forma normale prenessa

Definizione: una formula $\varphi$ è in forma normale prenessa (FNP) se è del tipo

$$ \mathcal Q_1 x_1\dots \mathcal Q_n x_n \psi $$

dove $\mathcal Q_i\in \{\forall , \exist\}$ e $\psi$ non contiene quantificatori. La sottoformula $\psi$ è detta matrice della formula $\varphi.$

Ad esempio:

• $\forall x\exist y(P(x, y)\rarr Q(c))$ è una formula chiusa in forma normale prenessa;
• $\forall x P(x, y)$ è una formula aperta (non chiusa) in forma normale prenessa;
• $P(x, y)\rarr \exist yQ(y)$ non è in forma normale prenessa perchè il conseguente dell’implicazione contiene un quantificatore.

Trasformazione in forma normale prenessa

Utilizzando le equivalenze logiche, è possibile trasformare ogni formula del primo ordine in una formula in forma normale prenessa, preservandone la verità rispetto a tutti i modelli e gli assegnamenti.

Proposizione: Per ogni formula $\varphi$ esiste una formula $\varphi^P$ in forma normale prenessa tale che $\varphi \equiv \varphi^P$.

La dimostrazione può essere fatta per induzione strutturale su $\varphi$.

• Esempio

Forma di Skolem

Definizione: Una formula è in forma di Skolem se è in forma normale premessa e non contiene quantificatori esistenziali, cioè se è del tipo

$$ \forall x_1\dots \forall x_n\psi $$

e $\psi$ è una matrice (non contiene quantificatori).

Si chiama skolemizzazione il processo che permette di ottenere una formula $\varphi^S$ in forma di Skolem a partire da una formula $\varphi$ in forma normale prenessa, eliminando i quantificatori esistenziali in maniera opportuna.

A differenza della forma normale prenessa, la forma di Skolem non preserva la verità della formula rispetto a tutti i modelli e gli assegnamenti (cioè non si ha l’equivalenza logica tra una formula e la sua forma di Skolem), ma preserva invece solo la soddisfacibilità.

Skolemizzazione