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 ${\displaystyle \qquad y}$, quantificada existencialmente, por um termo ${\displaystyle f(x_{1},\ldots ,x_{n})}$ no qual o símbolo de função ${\displaystyle \qquad f}$ é uma nova função (nao existe outra ocorrência dele na fórmula). Se a fórmula estiver na forma normal prenex, ${\displaystyle x_{1},\ldots ,x_{n}}$ são as variáveis universalmente quantificadas cujos quantificadores precedem a variável ${\displaystyle \qquad y}$. Podemos dizer que ${\displaystyle \exists y}$ cai sob o escopo dos quantificadores universais que o precedem. A função ${\displaystyle \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 ${\displaystyle \qquad y}$ quantificada existencialmente ${\displaystyle (\exists y)}$, onde essa quantificação não é precedida por um quantificador universal ${\displaystyle \forall x}$, então a variável ${\displaystyle \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.

${\displaystyle \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 ${\displaystyle \qquad \Phi }$ é satisfatível se existir um modelo ${\displaystyle \qquad M}$ tal que, para todo valor aplicado à variável livre ${\displaystyle \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, ${\displaystyle \forall x.R(x,f(x))}$ é satisfativel se e somente se existir um modelo ${\displaystyle \qquad M}$, que contenha um valor para ${\displaystyle \qquad f}$, tal que ${\displaystyle \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 ${\displaystyle \exists f\forall x.R(x,f(x))}$, que é satisfativelmente equivalente à ${\displaystyle \forall x\exists y.R(x,y)}$.

No meta-resultado, a satisfatibilidade de primeira ordem pode ser escrita como ${\displaystyle \exists M\forall \mu ~.~(M,\mu \models \Phi )}$, onde ${\displaystyle \qquad M}$ é um modelo e ${\displaystyle \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 ${\displaystyle \qquad \Phi }$ contém implicitamente um quantificador existencial ${\displaystyle \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 ${\displaystyle \exists f\forall x.R(x,f(x))}$ como ${\displaystyle \forall x.R(x,f(x))}$ pode ser realizada porque as funções estão implicitamente existencialmente quantificadas em ${\displaystyle \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 ${\displaystyle F_{1}=\forall x_{1}\dots \forall x_{n}\exists yR(x_{1},\dots ,x_{n},y)}$. Esta fórmula é satisfeita por um modelo ${\displaystyle \qquad M}$ se e somente se para todo possível valor de ${\displaystyle x_{1},\dots ,x_{n}}$, no modelo, existe um valor para ${\displaystyle \qquad y}$ que torne ${\displaystyle R(x_{1},\dots ,x_{n},y)}$ verdadeiro. Pelo axioma da escolha, existe uma função ${\displaystyle \qquad f}$ tal que ${\displaystyle y=f(x_{1},\dots ,x_{n})}$. Em consequência, a fórmula ${\displaystyle 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 ${\displaystyle \qquad f}$ a ${\displaystyle \qquad M}$. Isto mostra que ${\displaystyle F_{1}}$ é satisfatível somente se ${\displaystyle F_{2}}$ também for. De outra maneira, se ${\displaystyle F_{2}}$ for satisfatível, então existe um modelo ${\displaystyle \qquad M}$ que lhe satisfaça; este modelo aplica um valor à função ${\displaystyle \qquad f}$ tal que, para todo valor de ${\displaystyle x_{1},\dots ,x_{n}}$, a fórmula ${\displaystyle R(x_{1},\dots ,x_{n},f(x_{1},\dots ,x_{n}))}$ fica presa. Em conseqüência, ${\displaystyle F_{1}}$ é satisfeito pelo mesmo modelo pois pode fazer uma escolha para todo valor de ${\displaystyle x_{1},\ldots ,x_{n}}$, o valor ${\displaystyle y=f(x_{1},\dots ,x_{n})}$, onde o valor de ${\displaystyle \qquad f}$ é obtido de acordo com ${\displaystyle \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 ${\displaystyle \exists x.\Phi (x,y_{1},\ldots ,y_{n})}$ ocorrer em um tableau, onde ${\displaystyle x,y_{1},\ldots ,y_{n}}$ sejam variáveis livres de ${\displaystyle \Phi (x,y_{1},\ldots ,y_{n})}$, quando ${\displaystyle \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 à ${\displaystyle 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 ${\displaystyle \qquad \alpha }$, que está na forma normal prenex:

${\displaystyle \exists y.\forall x_{1}.\forall x_{2}.\exists z.R(y,x_{1},x_{2},z)}$

Eliminando os quantificadores existenciais em ${\displaystyle \qquad \alpha }$ por meio do processo de skolemização, obtemos a seguinte formula em sua forma normal Skolem:

${\displaystyle \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 ${\displaystyle \qquad y}$ foi substituída pela constante ${\displaystyle \qquad a}$, pois o quantificador existencial ${\displaystyle \exists y}$ não é precedido por nenhum quantificador universal. Já a variável ${\displaystyle \qquad z}$ foi substituída por um termo de função ${\displaystyle \qquad f(x_{1},x_{2})}$, já que o quantificador existencial ${\displaystyle \exists z}$ é precedido por duas quantificações universais, ${\displaystyle \forall x_{1}}$ e ${\displaystyle \forall x_{2}}$.

• 2. Considere a fórmula ${\displaystyle \qquad \beta }$, que está na forma normal prenex:

${\displaystyle \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 ${\displaystyle \qquad \beta }$ por meio do processo de skolemização, obtemos a seguinte fórmula em sua forma normal de Skolem:

${\displaystyle \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 ${\displaystyle \qquad x_{1}}$ foi substituída pelo termo de função ${\displaystyle \qquad f(x_{2},x_{4})}$ e a variável ${\displaystyle \qquad x_{5}}$ foi substituída pelo termo de outra função ${\displaystyle \qquad g(x_{2},x_{4},x_{3})}$.

Fazemos isso porque, na forma normal prenex:

Os quantificadores universais ${\displaystyle \forall x_{2}}$ e ${\displaystyle \forall x_{4}}$ precedem o quantificador existencial ${\displaystyle \exists x_{1}}$;

Os quantificadores universais ${\displaystyle \forall x_{2}}$ e ${\displaystyle \forall x_{4}}$ e ${\displaystyle \forall x_{3}}$ precedem o quantificador existencial ${\displaystyle \exists x_{5}}$.

Ver também

• Prolog
• Programação lógica
• Forma normal clausal
• Princípio da resolução
• Lógica de ordem superior

Ligações externas

• Skolemization on PlanetMath
• Skolem Function on MathWorld
• Skolemized Form on MathWorld