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 [editar]

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$ .

Usos da skolemização [editar]

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 [editar]

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)$ .