Lógicas Clássicas
Eliminação dos quantificadores existenciais (Skolemização ou Funções de Skolem)
- Quando uma fórmula está na forma normal Prenex, pode-se eliminar os quantificadores existenciais por uma função, se as variáveis estiverem no escopo do quantificador universal; caso estejam fora, substitui-se por uma constante.
- As constantes e funções usadas para substituir as variáveis existenciais são chamadas constante e funções de SkolemEx.: ?x ? y P(x,y)
Skolemizando: ?x P(x,f(x))
onde f(x) tem por único propósito garantir que existe algum valor (y) que depende de x pois está dentro do seu escopo. No entanto, se o quantificador existencial não residir no escopo do quantificador universal, como em ? y ?x P(x,y), a variável quantificada existencialmente será substituída por uma constante ?x P(x,a) que assegure sua existência, assim como sua independência de qualquer outra variável.