Skolemizzazione

In logica matematica, si dice skolemizzazione l'applicazione dell'algoritmo di Albert Thoralf Skolem che trasforma un enunciato in forma normale in un enunciato universale. L'enunciato in questione, dopo l'applicazione dell'algoritmo di Skolem, perde l'equivalenza semantica con l'enunciato di partenza. È interessante però constatare che rimane invariata la soddisfacibilità (ovvero, preso un qualsiasi enunciato $\phi$, esiste un modello per $\phi$ se e solo se ne esiste uno per la forma normale di Skolem di $\phi$).

Dato un linguaggio $L$, una frase $\alpha \in L$ è un enunciato universale se:

1. $\alpha$ è un enunciato (non ci sono variabili libere)
2. $\alpha$ è in forma normale e gli unici quantificatori, se esistono, sono di tipo $\forall$.

Esempio di enunciati universali.

• $A(b)\land C(a)$
• $\forall x\forall y(A(y)\land \neg C(x))$

N.B. L'algoritmo di Skolem non mantiene l'equivalenza semantica. La frase risultante dall'applicazione dell'algoritmo di Skolem è soddisfacibile se lo è la frase normale di partenza.

Algoritmo di Skolem

1. Trasformazione in forma prenessa. I quantificatori $\forall$ e $\exists$ devono essere raggruppati all'inizio della frase. $\forall x_{1},\exists x_{2}\forall x_{3}(\ldots )$
2. Determinare le variabili libere e vincolate. Nella frase non ci devono essere variabili libere, nel caso ci siano è necessario eseguire una sostituzione.
3. Se $Q_{1}$ (primo quantificatore) è $\forall$ si passa direttamente al punto successivo.
   Se $Q_{1}$ è $\exists$ allora si cancella $\exists x_{1}$ e si sostituisce ad ogni occorrenza di $x_{1}$ in $\alpha$ una stessa costante (nota come "costante di Skolem") che non compaia già in $\alpha$. Esempio: $\exists x\forall y(A(a,x)\land B(b,x,y)$ diventa $\forall y(A(a,c))\land B(b,c,y)$
   Come si può facilmente notare si è tolto il quantificatore $\exists$ e si è sostituita la variabile $x$ con la costante $c$.
   La scelta della costante $c$ non è casuale visto che $a$ e $b$ erano già utilizzate.
4. Prendo in rassegna $Q_{n}$
   • Se $Q_{n}$ è un $\forall$ si riparte da questo punto con $Q_{n+1}$.
   • Se $Q_{n}$ è $\exists$ allora i casi possono essere i seguenti:
     • Se il quantificatore $Q_{n-1}$ era di tipo $\exists$ ovvero $\exists x_{n-1}\exists {x_{n}}$ allora si ripete il punto precedente con $\exists x_{n}$ sostituendo però ad ogni occorrenza della variabile $x_{n}$ un funtore che prenda in rassegna tutte le variabili precedentemente utilizzate dai quantificatori $\forall$.
       Come si può notare finché non appaiono quantificatori di tipo $\forall$ si sostituiscono alle variabili $x_{n}$ delle semplici costanti.
     • Se il quantificatore $Q_{n-1}$ è di tipo $\forall$ ovvero $\forall x_{n-1}\exists x_{n}$ si cancella $\exists x_{n}$ e si sostituisce ogni occorrenza di $x_{n}$ in $\alpha$ con un funtore $f(\cdot )$ che prenda in rassegna le variabili utilizzate dai quantificatori $\forall$ che lo precedono. Se fosse $\forall y\forall z\exists u(\alpha )$ dovrei in primis cancellare $\exists u$ poi sostituire nella frase $\alpha$ la variabile $u$ con il funtore $f(y,z)$ (il funtore non deve esistere già).
   Esempio: $\forall x\exists y(A(x,f(x),y)\land C(y))$ diventa $\forall x(A(x,f(x),g(x))\land C(g(x)))$
   Come si può facilmente notare, si è tolto il quantificatore $\exists y$ e si è sostituita la variabile $y$ con il funtore $g(x)$.
   La scelta della variabile $x$ non è casuale, visto che $x_{1}$ in questo caso è proprio $x$.

Esempio pratico

$\exists x\forall y\forall z\exists u\forall t\exists v(\alpha )$

• Cancello $\exists x$ e dentro $\alpha$ sostituisco le $x$ con delle costanti (che non siano già state utilizzate)

Diventa $\forall y\forall z\exists u\forall t\exists v(\alpha ^{1})$ ($\alpha ^{1}$ è la nostra frase dopo aver applicato la sostituzione)

• Salto i due quantificatori $\forall$ e cancello il $\exists u$ ricordando di sostituire ogni occorrenza di $u$ in $\alpha ^{1}$ con un funtore (che non sia stato già utilizzato) che prende in rassegna le variabili utilizzate precedentemente dai quantificatori $\forall$. Nel nostro caso sarà $h(z,y)$.

Diventa $\forall y\forall z\forall t\exists v(\alpha ^{2})$ ($\alpha ^{2}$ è la nostra frase dopo aver applicato la sostituzione $u\rightarrow h(z,y)$)

• Rimane solo un ultimo quantificatore esistenziale, lo elimino e sostituisco in $\alpha ^{2}$ a tutte le occorrenze di $v$ un funtore che prenda in rassegna tutte le variabili utilizzate dai quantificatori universali utilizzati in precedenza. La sostituzione sarà $v\rightarrow i(y,z,t)$.

L'algoritmo terminerà quando i quantificatori saranno tutti del tipo $\forall$.