|
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 é satisfeirasatisfeita 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>
==Usos da skolemização==
|
