Forma normal prenex

Na lógica proposicional existem duas formas normais : a forma normal conjuntiva e a forma normal disjuntiva. Na lógica de predicados existe também uma forma normal chamada de forma normal prenex. A razão para utilizar uma forma normal prenex de uma fórmula usualmente é para simplificar métodos de prova, assim como as próprias fórmulas em si. Tal conceito é essêncial para desenvorlver a hierarquia aritmética e a hierarquia analítica.A prova de Gödel em seu teorema da completude para lógica de primeira ordem pré supõe que todas as fórmulas estão remodeladas em sua forma prenex.

Definição

Uma fórmula na lógica de predicados é dita estar em uma forma normal prenex se, e somente se, cada variável desta fórmula cai no escopo de algum quantificador , e se todos os quantificadores estão juntos precedendo uma sentença livre de quantificadores. Uma fórmula na forma normal prenex apresenta portanto a seguinte forma:

$\qquad Q_1 x_1 ... Q_n x_n .\alpha$

onde $\qquad \alpha$ é uma fórmula livre de quantificadores, chamada de matriz. A parte $\qquad Q_1 x_1 ... Q_n x_n$ é chamado de prefixo da fórmula, onde $\qquad x_1,...,x_n$ são variáveis distintas e $Q_i = \forall$ ou $Q_i = \exists$ para cada $1\le i\le n$. No caso em que todos os $\qquad Q_i$ são quantificadores universais, a fórmula é dita universalmente fechada.

Todas as fórmulas de primeira ordem são logicamente equivalentes a alguma fórmula na forma normal prenex. Por exemplo, sejam $\phi(y)$, $\psi(z)$, e $\rho(x)$ fórmulas sem quantificadores com suas respectivas variáveis livres. Têm-se a fórmula composta:

$\forall x ((\exists y \phi(y)) \lor ((\exists z \psi(z) ) \rightarrow \rho(x)))$

Podemos dizer que ela é equivalente à seguinte fórmula, que se encontra forma normal prenex:

$\forall x \exists y \forall z (\phi(y) \lor (\psi(z) \rightarrow \rho(x)))$

Podemos também definir a martiz da fórmula no formato prenex acima como: $\phi(y) \lor (\psi(z) \rightarrow \rho(x))$

Conversão para a Forma Normal Prenex

Existem várias regras de conversão que podem ser recursivamente aplicadas para converter uma fórmula para sua forma normal prenex. Tais regras dependem de quais conectivos lógicos aparecem na fórmula.

Conjunção e Disjunção

As regras para conjunção e disjunção dizem que:

$(\forall x \phi) \land \psi$ é equivalente à $\forall x ( \phi \land \psi)$,

$(\forall x \phi) \lor \psi$ é equivalente à $\forall x ( \phi \lor \psi)$;

e

$(\exists x \phi) \land \psi$ é equivalente à $\exists x (\phi \land \psi)$,

$(\exists x \phi) \lor \psi$ é equivalente à $\exists x (\phi \lor \psi)$.

Estas equivalencias são válidas desde que a variável atrelada ao respectivo quantificador não apareça como uma variável livre de ψ , e se aparecer , deve ser substituída por outra variável livre.

Por exemplo, na linguagem dos anéis:

$(\exists x (x^2 = 1)) \land (0 = y)$ é equivalente a $\exists x ( x^2 = 1 \land 0 = y)$,

porém

$(\exists x (x^2 = 1)) \land (0 = x)$ não é equivalente a $\exists x ( x^2 = 1 \land 0 = x)$

Por que para a formula à esquerda é verdade para qualquer anel quando a variável x é igual a 0, enquanto na fórmula a direita não há variáveis livre e é falsa em qualquer anel não trivial.

Negação

As regras para negação dizem que:

$\lnot \exists x \phi$ é equivalente a $\forall x \lnot \phi$ , uma vez que, se não há ao menos um x onde ɸ é verdade, então, para todo x, ɸ não é verdade, e

$\lnot \forall x \phi$ é equivalente a $\exists x \lnot \phi$, uma vez que, se nem para todo x, ɸ é verdadeiro, então para algum x, ɸ é falso.

Implicação

Há quarto regras para a implicação: duas que removem quantificadores do antecedente, e duas que removem os quantificadores do consequente. Essas regras podem ser encontradas reescrevendo a implicação $\phi \rightarrow \psi$ como $\lnot \phi \lor \psi$ e aplicando as regras de disjunção acima. Assim como as regras de disjunção, essas regras requerem que a variável quantificada em uma subfórmula não apareça livre na outra.

As regras para remover quantificadores dos antecedentes são:

$(\forall x \phi ) \rightarrow \psi$ é equivalente a $\exists x (\phi \rightarrow \psi)$,

$(\exists x \phi ) \rightarrow \psi$ é equivalente a $\forall x (\phi \rightarrow \psi)$.

As regras para remover quantificadores dos consequentes são:

$\phi \rightarrow (\exists x \psi)$ é equivalente a $\exists x (\phi \rightarrow \psi)$,

$\phi \rightarrow (\forall x \psi)$ é equivalente a $\forall x (\phi \rightarrow \psi)$.

Implicação Exemplificada

Suponha que $\phi$, $\psi$, e $\rho$ são formulas sem quantificadores e não há variáveis livres compartilhadas em duas delas. Considere a formula:

$(\phi \lor \exists x \psi) \rightarrow \forall z \rho$.

Aplicando a regra por recursividade, começando pela formula mais interna, a seguinte sequência de equivalências lógicas pode ser obtida:

$( \exists x (\phi \lor \psi) ) \rightarrow \forall z \rho$,

$\forall x ( ( \phi \lor \psi) \rightarrow \forall z \rho )$,

$\forall x ( \forall z (( \phi \lor \psi) \rightarrow \rho ))$,

$\forall x \forall z ( ( \phi \lor \psi) \rightarrow \rho )$.

Esta não é somente a única forma de encontrar a prenex da formula original. Por exemplo, ao lidar com os consequentes antes dos antecedentes no exemplo acima :

$\forall z ( (\phi \lor \exists x \psi) \rightarrow \rho )$

$\forall z ( (\exists x (\phi \lor \psi) ) \rightarrow \rho )$,

$\forall z ( \forall x ( (\phi \lor \psi) \rightarrow \rho ) )$,

$\forall z \forall x ( (\phi \lor \psi) \rightarrow \rho )$.

Exemplo

Seja $\qquad \alpha$ a fórmula:

$\lnot (\exists x .P(x,y) \rightarrow \exists x .\lnot (P(x,y) \land \exists y .R(y)))$

Uma seqüência de reduções para transformar a fórmula $\qquad \alpha$ numa fórmula na forma normal prenex é a seguinte:

$\twoheadrightarrow \lnot (\exists x .P(x,y) \rightarrow \exists x .\lnot (P(x,y) \land \exists y .R(y)))$

$\twoheadrightarrow \lnot (\exists x .P(x,y) \rightarrow \exists x .\lnot \exists y_1 .(P(x,y) \land R(y_1)))$

$\twoheadrightarrow \lnot (\exists x .P(x,y) \rightarrow \exists x .\forall y_1 .\lnot (P(x,y) \land R(y_1)))$

$\twoheadrightarrow \lnot \forall x_1 .(P(x_1,y) \rightarrow \exists x .\forall y_1 .\lnot (P(x,y) \land R(y_1)))$

$\twoheadrightarrow \lnot \forall x_1 .\exists x_2 .(P(x_1,y) \rightarrow \forall y_1 .\lnot (P(x_2,y) \land R(y_1)))$

$\twoheadrightarrow \lnot \forall x_1 .\exists x_2 .\forall y_1 .(P(x_1,y) \rightarrow \lnot (P(x_2,y) \land R(y_1)))$

$\twoheadrightarrow \exists x_1 .\lnot \exists x_2 .\forall y_1 .(P(x_1,y) \rightarrow \lnot (P(x_2,y) \land R(y_1)))$

$\twoheadrightarrow \exists x_1 .\forall x_2 .\lnot \forall y_1 .(P(x_1,y) \rightarrow \lnot (P(x_2,y) \land R(y_1)))$

$\twoheadrightarrow \exists x_1 .\forall x_2 .\exists y_1 .\lnot (P(x_1,y) \rightarrow \lnot (P(x_2,y) \land R(y_1)))$

Lógica Intuicionista

As regras para conversão em forma normal prenex nos faz usar pesadamente a lógica clássica. Na lógica intuicionista, não é verdade que toda fórmula é logicamente equivalente a uma forma prenex. A negação do conectivo é um obstáculo, mas não o único. O operador de implicação também é tradado diferente na lógica intuicionista, onde não é definida usando disjunção e negação. A interpretação BHK (Brouwer–Heyting–Kolmogorov interpretation) ilustra por que algumas fórmulas não possuem uma forma prenex intuicionalisticamente equivalente. A seguir, veja uma prova:

$(\exists x \phi) \rightarrow \exists y \psi \qquad (1)$

É uma função que, dado um concreto x e uma prova de φ(x), produz um concreto y and e uma prova de ψ(y). Neste caso, é permitível para o valor de y ser computado a partir do valor x.

$\exists y ( \exists x \phi \rightarrow \psi), \qquad (2)$

Agora, produzimos um único valor concreto y e a função que converte qualquer prova de $\exists x \phi$ em uma prova de ψ(y). Cada x satisfatível a φ pode ser usado para construer um y satisfatível a ψ, mas nenhum y pode ser construído sem o conhecimento de tal x, então a formula (1) não é equivalente a fórmula (2). As regras para conversão em forma prenex que falham na lógica intuicionista são:

(1) $\forall x (\phi \lor \psi)$ implies $(\forall x \phi) \lor \psi$,

(2) $\forall x (\phi \lor \psi)$ implies $\phi \lor (\forall x \psi)$,

(3) $(\forall x \phi) \rightarrow \psi$ implies $\exists x (\phi \rightarrow \psi)$,

(4) $\phi \rightarrow (\exists x \psi)$ implies $\exists x (\phi \rightarrow \psi)$,

(5) $\lnot \forall x \phi$ implies $\exists x \lnot \phi$,(x não aparece como uma variável livre de $\,\psi$ e (1) e (3); x não aparece como uma variável livre de $\,\phi$ em (2) e (4)).

Ver também

• Lógica
• Skolemização
• Forma Normal Clausal
• Princípio da Resolução

Ligações externas

• Prenex Form on PlanetMath
• Prenex Normal Form on MathWorld