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.


Definição

editar

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:

 

onde   é uma fórmula livre de quantificadores, chamada de matriz. A parte   é chamado de prefixo da fórmula, onde   são variáveis distintas e   ou   para cada  . No caso em que todos os   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  ,  , e   fórmulas sem quantificadores com suas respectivas variáveis livres. Têm-se a fórmula composta:

 

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

 

Podemos também definir a martiz da fórmula no formato prenexa acima como:  


Conversão para a Forma Normal prenexa

editar

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.


Conjunção e Disjunção

editar

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

  é equivalente à  ,
  é equivalente à  ;

e

  é equivalente à  ,
  é equivalente à  .

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:

  é equivalente a  ,

porém

  não é equivalente a  

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

editar

As regras para negação dizem que:

  é equivalente a   , uma vez que, se não há ao menos um x onde ɸ é verdade, então, para todo x, ɸ não é verdade, e
  é equivalente a  , uma vez que, se nem para todo x, ɸ é verdadeiro, então para algum x, ɸ é falso.


Implicação

editar

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   como   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:

  é equivalente a  ,
  é equivalente a  .

As regras para remover quantificadores dos consequentes são:

  é equivalente a  ,
  é equivalente a  .


Implicação Exemplificada

editar

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

 .

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

 ,
 ,
 ,
 .

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 :

 
 ,
 ,
 .

Exemplo

editar

Seja   a fórmula:

 

Uma seqüência de reduções para transformar a fórmula   numa fórmula na forma normal prenexa é a seguinte:

 
 
 
 
 
 
 
 
 


Lógica Intuicionista

editar

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:

 

É 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.

 

Agora, produzimos um único valor concreto y e a função que converte qualquer prova de   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)  ,
(2)  ,
(3)  ,
(4)  ,
(5)  ,(x não aparece como uma variável livre de   e (1) e (3); x não aparece como uma variável livre de   em (2) e (4)).

Ver também

editar

Ligações externas

editar