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

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: \;(\forall x)P(x)\rightarrow(\exists y)Q(y).
    O que será pedido ao longo da resolução (cada etapa a produzir):
  1. Eliminar a implicação.
  2. Mover a negação para dentro dos quantificadores (aplicar as leis de negação de quantificadores).
  3. Pôr a fórmula em Forma Normal Prenex (todas as quantificações à frente).
  4. Skolemizar (remover quantificadores existenciais substituindo por constantes ou funções de Skolem).

Passo 2

Eliminar a implicação. Regra usada: para quaisquer fórmulas A e B vale a equivalência
A\rightarrow B \equiv \neg A \vee B.
Aqui A é (\forall x)P(x) e B é (\exists y)Q(y). Aplicando a regra obtemos:
\neg(\forall x)P(x)\vee(\exists y)Q(y).
Explicação didática: a implicação diz “se todo x satisfaz P então existe um y com Q”. 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:
\neg(\forall x)\,\Phi(x)\equiv(\exists x)\neg\Phi(x), \qquad \neg(\exists x)\,\Phi(x)\equiv(\forall x)\neg\Phi(x).
Aplicando a primeira lei ao termo \neg(\forall x)P(x) obtemos:
(\exists x)\neg P(x)\vee(\exists y)Q(y).
Explicação didática: negar “para todo x, P(x)” é equivalente a “existe um x tal que não P(x)”. 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:
(\exists x)\neg P(x)\vee(\exists y)Q(y).
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:
(\exists x)\neg P(x)\vee(\exists y)Q(y)\equiv(\exists x)(\exists y)\bigl[\neg P(x)\vee Q(y)\bigr].
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): \exists x\exists y é equivalente a \exists y\exists x.

Passo 5

Skolemização — eliminar os quantificadores existenciais substituindo por símbolos de Skolem. Regra geral:
  • Se uma existência \exists z está no escopo de alguns quantificadores universais \forall u_1,\dots,\forall u_n, substitui‑se z por uma função de Skolem f(u_1,\dots,u_n).
  • Se não há quantificadores universais no escopo (como é o nosso caso: só restam existenciais), substitui‑se cada \exists por uma constante de Skolem (uma nova constante que não aparece em nenhuma outra parte).
    Na nossa fórmula prenex (\exists x)(\exists y)[\neg P(x)\vee Q(y)] não há \forall no escopo, logo usamos constantes de Skolem distintas c_1 e c_2. Substituindo obtemos a fórmula skolemizada (sem quantificadores):
\neg P(c_1)\vee Q(c_2),
onde c_1 e c_2 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 x e de y não depende de nenhum universal, basta escolher nomes fixos (constantes) que representem “um x que viola P” e “um y com Q”.

Resposta

\neg P(c_1)\vee Q(c_2)

Exercícios relacionados