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à^[1] (ovvero, preso un qualsiasi enunciato ${\displaystyle \phi }$, esiste un modello per ${\displaystyle \phi }$ se e solo se ne esiste uno per la forma normale di Skolem di ${\displaystyle \phi }$).^[2]

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

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

Esempio di enunciati universali.

• ${\displaystyle A(b)\land C(a)}$
• ${\displaystyle \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.

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

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

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

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

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

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

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

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

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