Entrada:
(\forallx)P(x) -> (\existsy)Q(y)
Saída:
Passo 1 - Eliminar implicação:
-(\forallx)P(x) v (\existsy)Q(y)
Passo 2 - Mover negação:
(\existsx)-P(x) v (\existsy)Q(y)
Passo 3 - Forma Normal Prenex:
(ヨx)(\existsy)[-P(x) v Q(y)]
Passo 4 - Skolemização:
-P(\mp@subsup{\textrm{C}}{1}{})\vee\textrm{Q(}\mp@subsup{\textrm{C}}{2}{})
onde C1, C2 são constantes de Skolem
(\forallx)P(x) -> (\existsy)Q(y)
Saída:
Passo 1 - Eliminar implicação:
-(\forallx)P(x) v (\existsy)Q(y)
Passo 2 - Mover negação:
(\existsx)-P(x) v (\existsy)Q(y)
Passo 3 - Forma Normal Prenex:
(ヨx)(\existsy)[-P(x) v Q(y)]
Passo 4 - Skolemização:
-P(\mp@subsup{\textrm{C}}{1}{})\vee\textrm{Q(}\mp@subsup{\textrm{C}}{2}{})
onde C1, C2 são constantes de Skolem
Passo 1
O enunciado nos dá a fórmula inicial e pede transformá‑la passo a passo até a forma sem quantificadores (Skolemização). Informação fornecida:
- Fórmula inicial:
.
O que será pedido ao longo da resolução (cada etapa a produzir):
- Eliminar a implicação.
- Mover a negação para dentro dos quantificadores (aplicar as leis de negação de quantificadores).
- Pôr a fórmula em Forma Normal Prenex (todas as quantificações à frente).
- Skolemizar (remover quantificadores existenciais substituindo por constantes ou funções de Skolem).
Passo 2
Eliminar a implicação. Regra usada: para quaisquer fórmulas
e
vale a equivalência
Aqui
é
e
é
. Aplicando a regra obtemos:
Explicação didática: a implicação diz “se todo
satisfaz
então existe um
com
”. A equivalência transforma isso numa disjunção onde negamos o antecedente ou mantemos o consequente.
Passo 3
Mover a negação para dentro dos quantificadores (leis de negação de quantificadores). As leis fundamentais são:
Aplicando a primeira lei ao termo
obtemos:
Explicação didática: negar “para todo
,
” é equivalente a “existe um
tal que não
”. Ao mover a negação para dentro, as letras de quantificador trocam conforme acima.
Passo 4
Colocar em Forma Normal Prenex (trazer todas as quantificações para a frente). Temos atualmente uma disjunção de duas fórmulas quantificadas:
Regra prática usada: quando aparecem quantificadores existenciais em diferentes ramos de uma disjunção, pode‑se reunir as existenciais à frente (escalonamento de quantificadores do mesmo tipo). Assim:
Observações didáticas: aqui não houve conflito de nomes de variáveis, mas se houvesse, deve‑se renomear variáveis ligadas para evitar ambiguidade. A ordem de duas existenciais é irrelevante (comutam):
é equivalente a
.
Passo 5
Skolemização — eliminar os quantificadores existenciais substituindo por símbolos de Skolem. Regra geral:
- Se uma existência
está no escopo de alguns quantificadores universais , substitui‑se por uma função de Skolem . - Se não há quantificadores universais no escopo (como é o nosso caso: só restam existenciais), substitui‑se cada
por uma constante de Skolem (uma nova constante que não aparece em nenhuma outra parte).
Na nossa fórmula prenexnão há no escopo, logo usamos constantes de Skolem distintas e . Substituindo obtemos a fórmula skolemizada (sem quantificadores):
onde
e
são constantes de Skolem novas (nomes arbitrários, distintos, que não aparecem na fórmula original). Explicação didática: como a existência de
e de
não depende de nenhum universal, basta escolher nomes fixos (constantes) que representem “um
que viola
” e “um
com
”.