Skolemização: diferenças entre revisões
Conteúdo apagado Conteúdo adicionado
Linha 18:
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 implicitamente quantificadas existencialmente no quantificador <math>\exists M</math> da definição de satisfatibilidade da logica de primeira ordem.
A exatidão da 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>y</math> que torne <math>R(x_1,\dots,x_n,y)</math> verdadeiro.
==Exemplo==
| |||