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