Forma normal prenex

Origem: Wikipédia, a enciclopédia livre.

Na lógica de predicados uma fórmula está na forma normal prenex 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.

[editar] Deslocando os quantificadores

Para pôr uma fórmula na forma normal prenex, movemos todos os quantificadores à esquerda dos conectivos lógicos $\lnot ,\land ,\lor ,\rightarrow$ . Se a fórmula contiver algum conectivo $\leftrightarrow$ , entao antes de proceder a este processo, devemos eliminar este conectivo da fórmula usando a redução:

$\alpha \leftrightarrow \beta \twoheadrightarrow (\alpha \rightarrow \beta ) \land (\beta \rightarrow \alpha )$

Para mover cada quantificador à esquerda de cada tipo destes conectivos devemos usar uma das reduções a seguir.

$\lnot \exists x .\alpha \twoheadrightarrow \forall x .\lnot \alpha$
$\lnot \forall x .\alpha \twoheadrightarrow \exists x .\lnot \alpha$
$\forall x .\alpha \land \beta \twoheadrightarrow \forall y .(\alpha [y/x] \land \beta )$
$\exists x .\alpha \land \beta \twoheadrightarrow \exists y .(\alpha [y/x] \land \beta )$
$\forall x .\alpha \lor \beta \twoheadrightarrow \forall y .(\alpha [y/x] \lor \beta )$
$\exists x .\alpha \lor \beta \twoheadrightarrow \exists y .(\alpha [y/x] \lor \beta )$
$\beta \land \forall x .\alpha \twoheadrightarrow \forall y .(\beta \land \alpha [y/x])$
$\beta \land \exists x .\alpha \twoheadrightarrow \exists y .(\beta \land \alpha [y/x])$
$\beta \lor \forall x .\alpha \twoheadrightarrow \forall y .(\beta \lor \alpha [y/x])$
$\beta \lor \exists x .\alpha \twoheadrightarrow \exists y .(\beta \lor \alpha [y/x])$
$\forall x .\alpha \rightarrow \beta \twoheadrightarrow \exists y .(\alpha [y/x] \rightarrow \beta )$
$\exists x .\alpha \rightarrow \beta \twoheadrightarrow \forall y .(\alpha [y/x] \rightarrow \beta )$
$\alpha \rightarrow \forall x .\beta \twoheadrightarrow \forall y .(\alpha \rightarrow \beta [y/x])$
$\alpha \rightarrow \exists x .\beta \twoheadrightarrow \exists y .(\alpha \rightarrow \beta [y/x])$

Observe que a renomeação de todas as variáveis é para se garantir que todas as variáveis diferentes tenham distintos nomes. Se não tivermos este cuidado, pode acontecer que a fórmula resultante não seja equivalente à original. Por exemplo, no caso da fórmula $\forall x .P(x) \land R(a,x)$ , se aplicarmos a redução (3) obtemos a fórmula $\forall y .(P(y) \land R(a,x))$ . Mas, senão tivessemos realizado a renomeação de variáveis, teriamos obtido a fórmula $\forall x .(P(x) \land R(a,x))$ , onde a ocorrência de variável $\qquad x$ em $\qquad R(a,x)$ , que antes era livre, passaria a ser ligada, alterando completamente o sentido da fórmula e portanto transformando a fórmula original numa fórmula não equivalente.

[editar] Exemplo

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)))$ ---------------------------redução (8)

$\twoheadrightarrow \lnot (\exists x .P(x,y) \rightarrow \exists x .\lnot \exists y_1 .(P(x,y) \land R(y_1)))$ ------------------------redução (1)

$\twoheadrightarrow \lnot (\exists x .P(x,y) \rightarrow \exists x .\forall y_1 .\lnot (P(x,y) \land R(y_1)))$ ------------------------redução (12)

$\twoheadrightarrow \lnot \forall x_1 .(P(x_1,y) \rightarrow \exists x .\forall y_1 .\lnot (P(x,y) \land R(y_1)))$ --------------------redução (14)

$\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)))$ ----------------redução (13)

$\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)))$ ----------------redução (2)

$\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)))$ ----------------redução (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)))$ ----------------redução (2)

$\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)))$

[editar] Veja também

[editar] Ligações externas

Retirado de "http://pt.wikipedia.org../../../f/o/r/Forma_normal_prenex.html"

Categoria: Lógica matemática

Forma normal prenex

Origem: Wikipédia, a enciclopédia livre.

Índice

[editar] Deslocando os quantificadores

[editar] Exemplo

[editar] Veja também

[editar] Ligações externas

Views

Navegação

Busca

Outras línguas