Skolemização: diferenças entre revisões

 

 

 

 

 

 

 

 

 

 

 

 

 

A exatidão do processo de skolemização é mostrada na fórmula <math>F_1 = \forall x_1 \dots \forall x_n \exists y R(x_1,\dots,x_n,y)</math>. Esta fórmula é satisfeita por um modelo <math>\qquad M</math> se e somente se para todo possível valor de <math>x_1,\dots,x_n</math>, no modelo, existe um valor para <math>\qquad y</math> que torne <math>R(x_1,\dots,x_n,y)</math> verdadeiro. Pelo axioma da escolha, existe uma função <math>\qquad f</math> tal que <math>y = f(x_1,\dots,x_n)</math>. Em consequência, a fórmula <math>F_2 = \forall x_1 \dots \forall x_n R(x_1,\dots,x_n,f(x_1,\dots,x_n))</math> é satisfatível, pois a mesma obteve um modelo ao se adicionar o valor de <math>\qquad f</math> a <math>\qquad M</math>. Isto mostra que <math>F_1</math> é satisfatível somente se <math>F_2</math> também for. De outra maneira, se <math>F_2</math> for satisfatível, então existe um modelo <math>\qquad M</math> que lhe satisfaça; este modelo aplica um valor à função <math>\qquad f</math> tal que, para todo valor de <math>x_1,\dots,x_n</math>, a fórmula <math>R(x_1,\dots,x_n,f(x_1,\dots,x_n))</math> fica presa. Em conseqüência, <math>F_1</math> é satisfeito pelo mesmo modelo pois pode fazer uma escolha para todo valor de <math>x_1,\ldots,x_n</math>, o valor <math>y=f(x_1,\dots,x_n)</math>, onde o valor de <math>\qquad f</math> é obtido de acordo com <math>\qquad M</math>.

 

 

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 <math>\exists x . \Phi(x,y_1,\ldots,y_n)</math> ocorrer em um tableau, onde <math>x,y_1,\ldots,y_n</math> sejam variáveis livres de <math>\Phi(x,y_1,\ldots,y_n)</math>, quando <math>\Phi(f(y_1,\ldots,y_n),y_1,\ldots,y_n)</math> 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 à <math>f</math> 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.

 

 

* 1.Considere a fórmula <math>\qquad \alpha</math> que esta na forma normal prenex:

Note que no processo de skolemização a variável <math>\qquad x_1</math> foi substituída pelo termo de função <math>\qquad f(x_2)</math> e não por <math>\qquad f(x_2, x_4)</math>, pois <math>\qquad x_4</math> não faz parte da mesma fórmula atômica de <math>\qquad x_1</math>.

 

 

 

* [[Lógica de ordem superior]]

 

* [http://planetmath.org/encyclopedia/Skolemization.html Skolemization on PlanetMath]

* [http://mathworld.wolfram.com/SkolemFunction.html Skolem Function on MathWorld]

[[ja:スコーレム標準形]]

[[pl:Skolemizacja]]

[[zh:斯科伦范式]]