Forma normal prenex

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa

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[editar | editar código-fonte]

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[editar | editar código-fonte]

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[editar | editar código-fonte]

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[editar | editar código-fonte]

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[editar | editar código-fonte]

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 \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[editar | editar código-fonte]

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[editar | editar código-fonte]

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[editar | editar código-fonte]

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[editar | editar código-fonte]

Ligações externas[editar | editar código-fonte]