Skolemização

Origem: Wikipédia, a enciclopédia livre.

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 através 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.

[editar] 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 y R(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$ .

[editar] 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 através 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.

[editar] Exemplos

1.Considere a fórmula $\qquad \alpha$ que esta 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$ através do processo de skolemização, obtemos a seguinte formula em sua forma normal Skolem:

$\forall x_1 .\forall x_2 (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 esta 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$ através 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_2) \rightarrow \lnot (P(x_3,x_4) \land R(a)))$

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)$ e não por $\qquad f(x_2, x_4)$ , pois $\qquad x_4$ não faz parte da mesma fórmula atômica de $\qquad x_1$ .