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 prenexa. A razão para utilizar uma forma normal prenexa de uma fórmula usualmente é para simplificar métodos de prova, assim como as próprias fórmulas em si. Tal conceito é essencial para desenvolver 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 prenexa.

Uma fórmula na lógica de predicados é dita estar em uma forma normal prenexa se, e só 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 prenexa apresenta portanto a seguinte forma:

Q 1 x 1 . . . Q n x n . α {\displaystyle \qquad Q_{1}x_{1}...Q_{n}x_{n}.\alpha }

onde α {\displaystyle \qquad \alpha } é uma fórmula livre de quantificadores, chamada de matriz. A parte Q 1 x 1 . . . Q n x n {\displaystyle \qquad Q_{1}x_{1}...Q_{n}x_{n}} é chamado de prefixo da fórmula, onde x 1 , . . . , x n {\displaystyle \qquad x_{1},...,x_{n}} são variáveis distintas e Q i = ∀ {\displaystyle Q_{i}=\forall } ou Q i = ∃ {\displaystyle Q_{i}=\exists } para cada 1 ≤ i ≤ n {\displaystyle 1\leq i\leq n} . No caso em que todos os Q i {\displaystyle \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 prenexa. Por exemplo, sejam ϕ ( y ) {\displaystyle \phi (y)} , ψ ( z ) {\displaystyle \psi (z)} , e ρ ( x ) {\displaystyle \rho (x)} fórmulas sem quantificadores com suas respectivas variáveis livres. Têm-se a fórmula composta:

∀ x ( ( ∃ y ϕ ( y ) ) ∨ ( ( ∀ z ψ ( z ) ) → ρ ( x ) ) ) {\displaystyle \forall x((\exists y\phi (y))\lor ((\forall z\psi (z))\rightarrow \rho (x)))}

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

∀ x ∃ y ∀ z ( ϕ ( y ) ∨ ( ψ ( z ) → ρ ( x ) ) ) {\displaystyle \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 prenexa acima como: ϕ ( y ) ∨ ( ψ ( z ) → ρ ( x ) ) {\displaystyle \phi (y)\lor (\psi (z)\rightarrow \rho (x))}

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

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

( ∀ x ϕ ) ∧ ψ {\displaystyle (\forall x\phi )\land \psi } é equivalente à ∀ x ( ϕ ∧ ψ ) {\displaystyle \forall x(\phi \land \psi )} ,

( ∀ x ϕ ) ∨ ψ {\displaystyle (\forall x\phi )\lor \psi } é equivalente à ∀ x ( ϕ ∨ ψ ) {\displaystyle \forall x(\phi \lor \psi )} ;

e

( ∃ x ϕ ) ∧ ψ {\displaystyle (\exists x\phi )\land \psi } é equivalente à ∃ x ( ϕ ∧ ψ ) {\displaystyle \exists x(\phi \land \psi )} ,

( ∃ x ϕ ) ∨ ψ {\displaystyle (\exists x\phi )\lor \psi } é equivalente à ∃ x ( ϕ ∨ ψ ) {\displaystyle \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:

( ∃ x ( x 2 = 1 ) ) ∧ ( 0 = y ) {\displaystyle (\exists x(x^{2}=1))\land (0=y)} é equivalente a ∃ x ( x 2 = 1 ∧ 0 = y ) {\displaystyle \exists x(x^{2}=1\land 0=y)} ,

porém

( ∃ x ( x 2 = 1 ) ) ∧ ( 0 = x ) {\displaystyle (\exists x(x^{2}=1))\land (0=x)} não é equivalente a ∃ x ( x 2 = 1 ∧ 0 = x ) {\displaystyle \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.

As regras para negação dizem que:

¬ ∃ x ϕ {\displaystyle \lnot \exists x\phi } é equivalente a ∀ x ¬ ϕ {\displaystyle \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

¬ ∀ x ϕ {\displaystyle \lnot \forall x\phi } é equivalente a ∃ x ¬ ϕ {\displaystyle \exists x\lnot \phi } , uma vez que, se nem para todo x, ɸ é verdadeiro, então para algum x, ɸ é falso.

Há quatro 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 ϕ → ψ {\displaystyle \phi \rightarrow \psi } como ¬ ϕ ∨ ψ {\displaystyle \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:

( ∀ x ϕ ) → ψ {\displaystyle (\forall x\phi )\rightarrow \psi } é equivalente a ∃ x ( ϕ → ψ ) {\displaystyle \exists x(\phi \rightarrow \psi )} ,

( ∃ x ϕ ) → ψ {\displaystyle (\exists x\phi )\rightarrow \psi } é equivalente a ∀ x ( ϕ → ψ ) {\displaystyle \forall x(\phi \rightarrow \psi )} .

As regras para remover quantificadores dos consequentes são:

ϕ → ( ∃ x ψ ) {\displaystyle \phi \rightarrow (\exists x\psi )} é equivalente a ∃ x ( ϕ → ψ ) {\displaystyle \exists x(\phi \rightarrow \psi )} ,

ϕ → ( ∀ x ψ ) {\displaystyle \phi \rightarrow (\forall x\psi )} é equivalente a ∀ x ( ϕ → ψ ) {\displaystyle \forall x(\phi \rightarrow \psi )} .

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

( ϕ ∨ ∃ x ψ ) → ∀ z ρ {\displaystyle (\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:

( ∃ x ( ϕ ∨ ψ ) ) → ∀ z ρ {\displaystyle (\exists x(\phi \lor \psi ))\rightarrow \forall z\rho } ,

∀ x ( ( ϕ ∨ ψ ) → ∀ z ρ ) {\displaystyle \forall x((\phi \lor \psi )\rightarrow \forall z\rho )} ,

∀ x ( ∀ z ( ( ϕ ∨ ψ ) → ρ ) ) {\displaystyle \forall x(\forall z((\phi \lor \psi )\rightarrow \rho ))} ,

∀ x ∀ z ( ( ϕ ∨ ψ ) → ρ ) {\displaystyle \forall x\forall z((\phi \lor \psi )\rightarrow \rho )} .

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

∀ z ( ( ϕ ∨ ∃ x ψ ) → ρ ) {\displaystyle \forall z((\phi \lor \exists x\psi )\rightarrow \rho )}

∀ z ( ( ∃ x ( ϕ ∨ ψ ) ) → ρ ) {\displaystyle \forall z((\exists x(\phi \lor \psi ))\rightarrow \rho )} ,

∀ z ( ∀ x ( ( ϕ ∨ ψ ) → ρ ) ) {\displaystyle \forall z(\forall x((\phi \lor \psi )\rightarrow \rho ))} ,

∀ z ∀ x ( ( ϕ ∨ ψ ) → ρ ) {\displaystyle \forall z\forall x((\phi \lor \psi )\rightarrow \rho )} .

Seja α {\displaystyle \qquad \alpha } a fórmula:

¬ ( ∃ x . P ( x , y ) → ∃ x . ¬ ( P ( x , y ) ∧ ∃ y . R ( y ) ) ) {\displaystyle \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 α {\displaystyle \qquad \alpha } numa fórmula na forma normal prenexa é a seguinte:

↠ ¬ ( ∃ x . P ( x , y ) → ∃ x . ¬ ( P ( x , y ) ∧ ∃ y . R ( y ) ) ) {\displaystyle \twoheadrightarrow \lnot (\exists x.P(x,y)\rightarrow \exists x.\lnot (P(x,y)\land \exists y.R(y)))}

↠ ¬ ( ∃ x . P ( x , y ) → ∃ x . ¬ ∃ y 1 . ( P ( x , y ) ∧ R ( y 1 ) ) ) {\displaystyle \twoheadrightarrow \lnot (\exists x.P(x,y)\rightarrow \exists x.\lnot \exists y_{1}.(P(x,y)\land R(y_{1})))}

↠ ¬ ( ∃ x . P ( x , y ) → ∃ x . ∀ y 1 . ¬ ( P ( x , y ) ∧ R ( y 1 ) ) ) {\displaystyle \twoheadrightarrow \lnot (\exists x.P(x,y)\rightarrow \exists x.\forall y_{1}.\lnot (P(x,y)\land R(y_{1})))}

↠ ¬ ∀ x 1 . ( P ( x 1 , y ) → ∃ x . ∀ y 1 . ¬ ( P ( x , y ) ∧ R ( y 1 ) ) ) {\displaystyle \twoheadrightarrow \lnot \forall x_{1}.(P(x_{1},y)\rightarrow \exists x.\forall y_{1}.\lnot (P(x,y)\land R(y_{1})))}

↠ ¬ ∀ x 1 . ∃ x 2 . ( P ( x 1 , y ) → ∀ y 1 . ¬ ( P ( x 2 , y ) ∧ R ( y 1 ) ) ) {\displaystyle \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})))}

↠ ¬ ∀ x 1 . ∃ x 2 . ∀ y 1 . ( P ( x 1 , y ) → ¬ ( P ( x 2 , y ) ∧ R ( y 1 ) ) ) {\displaystyle \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})))}

↠ ∃ x 1 . ¬ ∃ x 2 . ∀ y 1 . ( P ( x 1 , y ) → ¬ ( P ( x 2 , y ) ∧ R ( y 1 ) ) ) {\displaystyle \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})))}

↠ ∃ x 1 . ∀ x 2 . ¬ ∀ y 1 . ( P ( x 1 , y ) → ¬ ( P ( x 2 , y ) ∧ R ( y 1 ) ) ) {\displaystyle \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})))}

↠ ∃ x 1 . ∀ x 2 . ∃ y 1 . ¬ ( P ( x 1 , y ) → ¬ ( P ( x 2 , y ) ∧ R ( y 1 ) ) ) {\displaystyle \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})))}

As regras para conversão em forma normal prenexa 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 prenexa. 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 prenexa intuicionalisticamente equivalente. A seguir, veja uma prova:

( ∃ x ϕ ) → ∃ y ψ ( 1 ) {\displaystyle (\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.

∃ y ( ∃ x ϕ → ψ ) , ( 2 ) {\displaystyle \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 ∃ x ϕ {\displaystyle \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 prenexa que falham na lógica intuicionista são:

(1) ∀ x ( ϕ ∨ ψ ) → ( ∀ x ϕ ) ∨ ψ {\displaystyle \forall x(\phi \lor \psi )\rightarrow (\forall x\phi )\lor \psi } ,

(2) ∀ x ( ϕ ∨ ψ ) → ϕ ∨ ( ∀ x ψ ) {\displaystyle \forall x(\phi \lor \psi )\rightarrow \phi \lor (\forall x\psi )} ,

(3) ( ∀ x ϕ ) → ψ → ∃ x ( ϕ → ψ ) {\displaystyle (\forall x\phi )\rightarrow \psi \rightarrow \exists x(\phi \rightarrow \psi )} ,

(4) ϕ → ( ∃ x ψ ) → ∃ x ( ϕ → ψ ) {\displaystyle \phi \rightarrow (\exists x\psi )\rightarrow \exists x(\phi \rightarrow \psi )} ,

(5) ¬ ∀ x ϕ → ∃ x ¬ ϕ {\displaystyle \lnot \forall x\phi \rightarrow \exists x\lnot \phi } ,(x não aparece como uma variável livre de ψ {\displaystyle \,\psi } e (1) e (3); x não aparece como uma variável livre de ϕ {\displaystyle \,\phi } em (2) e (4)).

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

• «Prenex Form on PlanetMath» 
• «Prenex Normal Form on MathWorld» 

• Portal da matemática