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 , e são quantificadores livre das fórmulas com variáveis livres mostrado, em seguida,
está na forma normal prenex com matriz , enquanto
é logicamente equivalente, mas não está na forma normal prenex.
A conversão de forma prenex
[editar | editar código-fonte]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
[editar | editar código-fonte]As regras de conjunção e disjunção, dizem que
- é equivalente a ,
- é equivalente a ;
e
- é equivalente a ,
- é equivalente a .
As equivalências são válidas quando não aparece como uma variável livre de ; se aparece livre em pode-se mudar o nome do dependente no e obter o equivalente .
Por exemplo, na linguagem dos anéis,
- é equivalente a ,
mas
- não é equivalente a
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, vai ser o primeiro reescrito como e, em seguida, será colocado na forma normal prenex .
Negação
[editar | editar código-fonte]As regras para a negação dizem que
- é equivalente a
e
- é equivalente a .
Implicação
[editar | editar código-fonte]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 como 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:
- é equivalente a ,
- é equivalente a .
As regras de remoção dos quantificadores do conseqüente são:
- é equivalente a ,
- é equivalente a .
Exemplo
[editar | editar código-fonte]Suponha que , e são quantificadores livre de fórmulas e nenhuma dessas fórmulas compartilham qualquer variável. Considere a fórmula
- .
Recursivamente aplicando as regras, e começando nas subfórmulas mais internas, a seguinte seqüência de fórmulas logicamente equivalentes podem ser obtidas:
- .
- ,
- ,
- ,
- ,
- ,
- ,
- .
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
pode ser obtida:
- ,
- ,
- .
A lógica intuicionista
[editar | editar código-fonte]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
é uma função que, dado um x concreto e uma prova de , 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
por outro lado, produz um único valor concreto de y e uma função que converte qualquer prova de 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) implica ,
- (2) implica ,
- (3) implica ,
- (4) implica ,
- (5) implica ,
(x não aparece como uma variável de em (1) e (3); x não aparece como uma variável de em (2) e (4)).
Uso da forma prenex
[editar | editar código-fonte]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
[editar | editar código-fonte]Referências
[editar | editar código-fonte]- Hinman, P. (2005), Fundamentals of Mathematical Logic, ISBN 978-1-56881-262-5, A K Peters
|ISBN=
e|isbn=
redundantes (ajuda)