Usuário(a):Sheyla Souza/FNP - Forma Normal Prenex

Uma fórmula de cálculo de predicado está em prenex forma normal se está escrito como uma cadeia de quantificadores (referida como prefixo) seguido por um quantificador-parte livre (referida como matriz).

Cada fórmula na lógica clássica é equivalente a uma fórmula na forma normal prenex. Por exemplo, se ${\displaystyle }$, ${\displaystyle }$e ${\displaystyle }$ são quantificadores livre das fórmulas com variáveis livres mostrado, em seguida,

${\displaystyle }$

está na forma normal prenex com matriz ${\displaystyle }$, enquanto

${\displaystyle }$

é logicamente equivalente, mas não está na forma normal prenex.

A conversão de forma prenex

Toda fórmula de primeira ordem é logicamente equivalente (na lógica clássica) para alguma fórmula na forma normal prenex. Existem várias regras de conversão que podem ser aplicadas recursivamente para converter uma fórmula para a forma normal prenex. As regras dependem de qual conectivos lógicos aparecem na fórmula.

Conjunção e disjunção

As regras de conjunção e disjunção, dizem que

${\displaystyle }$ é equivalente a ${\displaystyle }$,

${\displaystyle }$ é equivalente a ${\displaystyle }$;

e

${\displaystyle }$ é equivalente a ${\displaystyle }$,

${\displaystyle }$ é equivalente a ${\displaystyle }$.

As equivalências são válidas quando ${\displaystyle }$ não aparece como uma variável livre de ${\displaystyle }$; se ${\displaystyle }$ aparece livre em ${\displaystyle }$pode-se mudar o nome do dependente ${\displaystyle }$ no ${\displaystyle }$ e obter o equivalente ${\displaystyle }$.

Por exemplo, na linguagem dos anéis,

${\displaystyle }$ é equivalente a ${\displaystyle }$,

mas

${\displaystyle }$ não é equivalente a ${\displaystyle }$

porque a fórmula da esquerda é verdadeira em qualquer anel quando a variável livre x é igual a 0, enquanto a fórmula da direita não tem variáveis livres e é falsa em qualquer anel não trivial. Então, ${\displaystyle }$ vai ser o primeiro reescrito como ${\displaystyle }$ e, em seguida, será colocado na forma normal prenex ${\displaystyle }$.

Negação

As regras para a negação dizem que

${\displaystyle }$ é equivalente a ${\displaystyle }$

e

${\displaystyle }$ é equivalente a ${\displaystyle }$.

Implicação

Existem quatro regras para a implicação: duas que removem quantificadores do antecedente e duas que removem quantificadores do conseqüente. Essas regras podem ser derivadas por reescrever a implicação ${\displaystyle }$ como ${\displaystyle }$ e aplicando as regras de disjunção acima. Como acontece com as regras de disjunção, essas regras exigem que a variável quantificada em uma subfórmula não aparece livre em outra subfórmula.

As regras de remoção dos quantificadores do antecedente são:

${\displaystyle }$ é equivalente a ${\displaystyle }$,

${\displaystyle }$ é equivalente a ${\displaystyle }$.

As regras de remoção dos quantificadores do conseqüente são:

${\displaystyle }$ é equivalente a ${\displaystyle }$,

${\displaystyle }$ é equivalente a ${\displaystyle }$.

Exemplo

Suponha que ${\displaystyle }$, ${\displaystyle }$e ${\displaystyle }$ são quantificadores livre de fórmulas e nenhuma dessas fórmulas compartilham qualquer variável. Considere a fórmula

${\displaystyle }$.

Recursivamente aplicando as regras, e começando nas subfórmulas mais internas, a seguinte seqüência de fórmulas logicamente equivalentes podem ser obtidas:

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

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

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

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

$\forall x(\neg (\phi \lor \psi )\lor \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 é a única forma prenex equivalente à fórmula original. Por exemplo, ao lidar com a consequente antes de o antecedente no exemplo acima, a forma prenex

${\displaystyle }$

pode ser obtida:

${\displaystyle }$

${\displaystyle }$,

${\displaystyle }$,

${\displaystyle }$.

A lógica intuicionista

As regras para a conversão de uma fórmula para forma prenex fazem uso intenso da lógica clássica. Na lógica intuicionista, não é verdade que cada fórmula é logicamente equivalente a uma fórmula prenex. A negação do conectivo é um obstáculo, mas não o único. O operador de implicação também é tratado de forma diferente na lógica intuicionista de lógica clássica; na lógica intuicionista, não é definível usando disjunção e negação.

O BHK interpretação ilustra por que algumas fórmulas não tem prenex intuitivamente-equivalente. Nesta interpretação, uma prova de

${\displaystyle }$

é uma função que, dado um x concreto e uma prova de ${\displaystyle }$, produz um y concreto e uma prova de ψ(y). Neste caso, é admissível para o valor de y para ser computado a partir do dado valor de x. Uma prova de

${\displaystyle }$

por outro lado, produz um único valor concreto de y e uma função que converte qualquer prova de ${\displaystyle }$ em uma prova de ψ(y). Se cada x satisfazendo φ pode ser usado para construir um y satisfazendo ψ mas não como y pode ser construído sem o conhecimento de um tal x , em seguida, fórmula (1) não é equivalente à fórmula (2).

As regras para converter uma fórmula para forma prenex falham na lógica intuicionista são:

(1) ${\displaystyle }$ implica ${\displaystyle }$,

(2) ${\displaystyle }$ implica ${\displaystyle }$,

(3) ${\displaystyle }$ implica ${\displaystyle }$,

(4) ${\displaystyle }$ implica ${\displaystyle }$,

(5) ${\displaystyle }$ implica ${\displaystyle }$,

(x não aparece como uma variável de ${\displaystyle }$ em (1) e (3); x não aparece como uma variável de ${\displaystyle }$ em (2) e (4)).

Uso da forma prenex

Alguns cálculos de provas terão que lidar apenas com uma teoria cujas fórmulas são escritos na forma normal prenex. O conceito é essencial para o desenvolvimento da hierarquia aritmética e a hierarquia analítica.

A prova de Gödel do teorema da completude para a lógica de primeira ordem pressupõe que todas as fórmulas foram reformuladas na forma normal prenex.

Veja também

• Herbrandização
• Skolemização
• Hierarquia aritmética

Referências

• Hinman, P. (2005), Fundamentals of Mathematical Logic, ISBN 978-1-56881-262-5, A K Peters