# Skolemização

Uma fórmula da lógica de primeira ordem está na forma normal de Skolem (nome devido à Thoralf Skolem), se sua forma normal prenex contiver somente quantificadores universais. Cada fórmula de primeira ordem pode ser convertida na forma normal de Skolem por meio do processo de skolemização. A fórmula resultante deste processo não é necessariamente equivalente à original, mas é satisfatível se e somente se a original também o for.
A skolemização é feita substituindo cada variável $\qquad y$, quantificada existencialmente, por um termo $f(x_{1},\ldots ,x_{n})$ no qual o símbolo de função $\qquad f$ é uma nova função (nao existe outra ocorrência dele na fórmula). Se a fórmula estiver na forma normal prenex, $x_{1},\ldots ,x_{n}$ são as variáveis universalmente quantificadas cujos quantificadores precedem a variável $\qquad y$. Podemos dizer que $\exists y$ cai sob o escopo dos quantificadores universais que o precedem. A função $\qquad f$ introduzida nesse processo é dita função de Skolem e o termo é dito termo de Skolem.
No caso da ocorrência de uma variável $\qquad y$ quantificada existencialmente $(\exists y)$, onde essa quantificação não é precedida por um quantificador universal $\forall x$, então a variável $\qquad y$ é substituída por uma constante.

## Como funciona

A skolemização trabalha aplicando a relação de equivalência da lógica de segunda ordem juntamente com a definição de satisfatibilidade da primeira ordem. A equivalência é feita "movendo" o quantificador existencial para antes do quantificador universal.
                               $\forall x\exists y.R(x,y)\iff \exists f\forall x.R(x,f(x)){\mbox{.}}$
Intuitivamente, a sentença "Para todo x existe um y tal que R(x,y)" é convertida para a forma equivalente "Existe uma função f em x, introduzida por y, para todo x preso no escopo de R(x,f(x))".
Esta equivalência é útil pois a definição de satisfatibilidade da lógica de primeira ordem é implícita nos quantificadores existenciais sobre um símbolo de função. Em resumo, uma fórmula de primeira ordem $\qquad \Phi$ é satisfatível se existir um modelo $\qquad M$ tal que, para todo valor aplicado à variável livre $\qquad \mu$ da fórmula, a fórmula seja verdadeira. Desde que o modelo contenha o valor de todos os símbolos de função, toda função de Skolem é implicitamente existencialmente quantificada. No exemplo acima, $\forall x.R(x,f(x))$ é satisfativel se e somente se existir um modelo $\qquad M$, que contenha um valor para $\qquad f$, tal que $\forall x.R(x,f(x))$ é verdade para todos os possíveis valores de suas variáveis livres (neste caso nenhuma). Esta mesma fórmula pode ser expressa em segunda ordem como $\exists f\forall x.R(x,f(x))$, que é satisfativelmente equivalente à $\forall x\exists y.R(x,y)$.
No meta-resultado, a satisfatibilidade de primeira ordem pode ser escrita como $\exists M\forall \mu ~.~(M,\mu \models \Phi )$, onde $\qquad M$ é um modelo e $\qquad \mu$ é o valor da variável. Desde que os modelos de primeira ordem contenham o valor de todo símbolo de função, toda função de Skolem $\qquad \Phi$ contém implicitamente um quantificador existencial $\exists M$. Em conseqüência, após ter substituído o quantificador existencial sobre variáveis que estão quantificadas existencialmente em funções na parte frontal da fórmula, a fórmula ainda pode ser tratada como sendo de primeira ordem removendo estes quantificadores existenciais. Esta etapa final do tratamento $\exists f\forall x.R(x,f(x))$ como $\forall x.R(x,f(x))$ pode ser realizada porque as funções estão implicitamente existencialmente quantificadas em $\exists M$ de acordo com definição de satisfatibilidade da lógica de primeira ordem.
A exatidão do processo de skolemização é mostrada na fórmula $F_{1}=\forall x_{1}\dots \forall x_{n}\exists yR(x_{1},\dots ,x_{n},y)$. Esta fórmula é satisfeita por um modelo $\qquad M$ se e somente se para todo possível valor de $x_{1},\dots ,x_{n}$, no modelo, existe um valor para $\qquad y$ que torne $R(x_{1},\dots ,x_{n},y)$ verdadeiro. Pelo axioma da escolha, existe uma função $\qquad f$ tal que $y=f(x_{1},\dots ,x_{n})$. Em consequência, a fórmula $F_{2}=\forall x_{1}\dots \forall x_{n}R(x_{1},\dots ,x_{n},f(x_{1},\dots ,x_{n}))$ é satisfatível, pois a mesma obteve um modelo ao se adicionar o valor de $\qquad f$ a $\qquad M$. Isto mostra que $F_{1}$ é satisfatível somente se $F_{2}$ também for. De outra maneira, se $F_{2}$ for satisfatível, então existe um modelo $\qquad M$ que lhe satisfaça; este modelo aplica um valor à função $\qquad f$ tal que, para todo valor de $x_{1},\dots ,x_{n}$, a fórmula $R(x_{1},\dots ,x_{n},f(x_{1},\dots ,x_{n}))$ fica presa. Em conseqüência, $F_{1}$ é satisfeito pelo mesmo modelo pois pode fazer uma escolha para todo valor de $x_{1},\ldots ,x_{n}$, o valor $y=f(x_{1},\dots ,x_{n})$, onde o valor de $\qquad f$ é obtido de acordo com $\qquad M$.

## Usos da skolemização

Um dos usos da skolemização é a prova automatizada de teoremas. Por exemplo, no método analítico de tableaux, sempre que uma fórmula cujo quantificador principal é o existencial, a fórmula obtida removendo esse quantificador por meio da skolemização pode ser gerada. Por exemplo, se $\exists x.\Phi (x,y_{1},\ldots ,y_{n})$ ocorrer em um tableau, onde $x,y_{1},\ldots ,y_{n}$ sejam variáveis livres de $\Phi (x,y_{1},\ldots ,y_{n})$, quando $\Phi (f(y_{1},\ldots ,y_{n}),y_{1},\ldots ,y_{n})$ puder ser adicionado à mesma ramificação do tableau. Esta adição não altera a sua satisfatibilidade: todo modelo da fórmula antiga pode ser expandido, adicionando um valor apropriado à $f$ em um modelo da nova fórmula.
Esta forma de skolemização é atualmente um progresso da skolemização "clássica", na qual todas as variáveis livres na fórmula são substituidas por um termo de Skolem. Esta é uma melhoria porque a semântica de tableau pode implicitamente colocar a fórmula no escopo de algumas variáveis quantificadas universalmente, que não estão em sua fórmula; estas variáveis não fazem parte de um termo de Skolem, quando deveriam fazer, de acordo com a definição original de skolemização. Uma outra melhoria que pode ser usada é aplicar o mesmo símbolo de uma função de Skolem para as fórmulas que são idênticas.

## Exemplos

* 1. Considere a fórmula $\qquad \alpha$, que está na forma normal prenex:
       $\exists y.\forall x_{1}.\forall x_{2}.\exists z.R(y,x_{1},x_{2},z)$
Eliminando os quantificadores existenciais em $\qquad \alpha$ por meio do processo de skolemização, obtemos a seguinte formula em sua forma normal Skolem:
       $\forall x_{1}.\forall x_{2}R(a,x_{1},x_{2},f(x_{1},x_{2}))$
Note que no processo de skolemização a variável $\qquad y$ foi substituída pela constante $\qquad a$, pois o quantificador existencial $\exists y$ não é precedido por nenhum quantificador universal. Já a variável $\qquad z$ foi substituída por um termo de função $\qquad f(x_{1},x_{2})$, já que o quantificador existencial $\exists z$ é precedido por duas quantificações universais, $\forall x_{1}$ e $\forall x_{2}$.
* 2. Considere a fórmula $\qquad \beta$, que está na forma normal prenex:
       $\forall x_{2}.\forall x_{4}.\exists x_{1}.\forall x_{3}.\exists x_{5}.\lnot (P(x_{1},x_{2})\rightarrow \lnot (P(x_{3},x_{4})\land R(x_{5})))$
Eliminando os quantificadores existenciais em $\qquad \beta$ por meio do processo de skolemização, obtemos a seguinte fórmula em sua forma normal de Skolem:
       $\forall x_{2}.\forall x_{4}.\forall x_{3}.\lnot (P(f(x_{2},x_{4}),x_{2})\rightarrow \lnot (P(x_{3},x_{4})\land R(g(x_{2},x_{4},x_{3}))))$
Note que:
No processo de skolemização, a variável $\qquad x_{1}$ foi substituída pelo termo de função $\qquad f(x_{2},x_{4})$ e a variável $\qquad x_{5}$ foi substituída pelo termo de outra função $\qquad g(x_{2},x_{4},x_{3})$.
Fazemos isso porque, na forma normal prenex:
Os quantificadores universais $\forall x_{2}$ e $\forall x_{4}$ precedem o quantificador existencial $\exists x_{1}$;
Os quantificadores universais $\forall x_{2}$ e $\forall x_{4}$ e $\forall x_{3}$ precedem o quantificador existencial $\exists x_{5}$.