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

Note que no processo de skolemização a variável <math>\qquad y</math> foi substituída pela constante <math>\qquad a</math>, pois o quantificador existencial <math>\exists y</math> não é precedido depor nenhum quantificador universal. Já a variável <math>\qquad z</math> foi substituída por um termo de função <math>\qquad f(x_1 ,x_2)</math>, já que o quantificador existencial <math>\exists z</math> é precedido por duas quantificações universais, <math>\forall x_1</math> e <math>\forall x_2</math>.