Revisão das 17h50min de 17 de dezembro de 2006 editar 201.73.157.197 (discussão) →‎Como funciona ← Ver a alteração anterior		Revisão das 18h40min de 17 de dezembro de 2006 editar desfazer 201.73.157.197 (discussão) →‎Como funciona Ver a alteração posterior →
Linha 10: ==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. Linha 17: 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 <math>\qquad \Phi</math> é satisfatível se existir um modelo <math>\qquad M</math> tal que, para todo valor aplicado à variável livre <math>\qquad \mu</math> 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, <math>\forall x . R(x,f(x))</math> é satisfativel se e somente se existir um modelo <math>\qquad M</math>, que contenha um valor para <math>\qquad f</math>, tal que <math>\forall x . R(x,f(x))</math> é 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 <math>\exists f \forall x . R(x,f(x))</math>, que é satisfativelmente equivalente à <math>\forall x \exists y . R(x,y)</math>. No meta-resultado, a satisfatibilidade de primeira ordem pode ser escrita como <math>\exists M \forall \mu ~.~ ( M,\mu \models \Phi )</math>, onde <math>\qquad M</math> é um modelo e <math>\qquad \mu</math> é 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 <math>\qquad \Phi</math> contém implicitamente um quantificador existencial <math>\exists M</math>. 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 <math>\exists f \forall x . R(x,f(x))</math> como <math>\forall x . R(x,f(x))</math> pode ser realizada porque as funções estão implicitamente ~~quantificadas~~ existencialmente noquantificadas ~~quantificador~~em <math>\exists M</math> dade acordo com definição de satisfatibilidade da ~~logica~~lógica de primeira ordem. A exatidão dado 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 é satisfeira por um modelo <math>\qquad M</math> se e somente se, para cada 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 a 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> ==Exemplo==

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