Forma normal Prenex - Prenex normal form

Uma fórmula do cálculo de predicado está na forma normal prenex ( PNF ) se for escrita como uma sequência de quantificadores e variáveis ​​ligadas , chamada de prefixo , seguida por uma parte livre de quantificador, chamada de matriz .

Cada fórmula na lógica clássica é equivalente a uma fórmula na forma normal prenex. Por exemplo, se , e são fórmulas sem quantificador com as variáveis ​​livres mostradas, então ${\ displaystyle \ phi (y)}$${\ displaystyle \ psi (z)}$${\ displaystyle \ rho (x)}$

${\ displaystyle \ forall x \ exists y \ forall z (\ phi (y) \ lor (\ psi (z) \ rightarrow \ rho (x)))}$

está na forma normal prenex com matriz , enquanto ${\ displaystyle \ phi (y) \ lor (\ psi (z) \ rightarrow \ rho (x))}$

${\ displaystyle \ forall x ((\ existe y \ phi (y)) \ lor ((\ existe z \ psi (z)) \ rightarrow \ rho (x)))}$

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

Conversão para forma prenex

Cada fórmula de primeira ordem é logicamente equivalente (na lógica clássica) a 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 quais conectivos lógicos aparecem na fórmula.

Conjunção e disjunção

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

${\ displaystyle (\ forall x \ phi) \ land \ psi}$ é equivalente a uma condição adicional (leve) ou, de forma equivalente, (significando que existe pelo menos um indivíduo), ${\ displaystyle \ forall x (\ phi \ land \ psi)}$${\ displaystyle \ existe x \ top}$${\ displaystyle \ lnot \ forall x \ bot}$

${\ displaystyle (\ forall x \ phi) \ lor \ psi}$ é equivalente a ; ${\ displaystyle \ forall x (\ phi \ lor \ psi)}$

e

${\ displaystyle (\ exists x \ phi) \ land \ psi}$ é equivalente a , ${\ displaystyle \ exists x (\ phi \ land \ psi)}$

${\ displaystyle (\ exists x \ phi) \ lor \ psi}$ é equivalente a sob condição adicional . ${\ displaystyle \ exists x (\ phi \ lor \ psi)}$${\ displaystyle \ existe x \ top}$

As equivalências são válidas quando não aparece como variável livre de ; se aparecer livre em , pode-se renomear o limite em e obter o equivalente . ${\ displaystyle x}$${\ displaystyle \ psi}$${\ displaystyle x}$${\ displaystyle \ psi}$${\ displaystyle x}$${\ displaystyle (\ exists x \ phi)}$${\ displaystyle (\ exists x '\ phi [x / x'])}$

Por exemplo, na linguagem dos anéis ,

${\ displaystyle (\ exists x (x ^ {2} = 1)) \ land (0 = y)}$ é equivalente a , ${\ displaystyle \ exists x (x ^ {2} = 1 \ land 0 = y)}$

mas

${\ displaystyle (\ exists x (x ^ {2} = 1)) \ land (0 = x)}$ não é equivalente a ${\ displaystyle \ existe x (x ^ {2} = 1 \ land 0 = x)}$

porque a fórmula à esquerda é verdadeira em qualquer anel quando a variável livre x é igual a 0, enquanto a fórmula à direita não tem variáveis ​​livres e é falsa em qualquer anel não trivial. Portanto , será primeiro reescrito como e depois colocado na forma normal prenex . ${\ displaystyle (\ exists x (x ^ {2} = 1)) \ land (0 = x)}$${\ displaystyle (\ exists x '(x' ^ {2} = 1)) \ land (0 = x)}$${\ displaystyle \ exists x '(x' ^ {2} = 1 \ land 0 = x)}$

Negação

As regras para negação dizem que

${\ displaystyle \ lnão \ existe x \ phi}$ é equivalente a ${\ displaystyle \ forall x \ lnot \ phi}$

e

${\ displaystyle \ lnot \ forall x \ phi}$ é equivalente a . ${\ displaystyle \ existing x \ lnot \ phi}$

Implicação

Existem quatro regras de implicação : duas que removem os quantificadores do antecedente e duas que removem os quantificadores do consequente. Essas regras podem ser obtidos por reescrever a implicação como e aplicação das regras de disjunção acima. Tal como acontece com as regras para disjunção, essas regras exigem que a variável quantificada em uma subfórmula não apareça livre na outra subfórmula. ${\ displaystyle \ phi \ rightarrow \ psi}$${\ displaystyle \ lnot \ phi \ lor \ psi}$

As regras para remover quantificadores do antecedente são (observe a mudança de quantificadores):

${\ displaystyle (\ forall x \ phi) \ rightarrow \ psi}$ é equivalente a (supondo que ), ${\ displaystyle \ exists x (\ phi \ rightarrow \ psi)}$${\ displaystyle \ existe x \ top}$

${\ displaystyle (\ exists x \ phi) \ rightarrow \ psi}$ é equivalente a . ${\ displaystyle \ forall x (\ phi \ rightarrow \ psi)}$

As regras para remover quantificadores do consequente são:

${\ displaystyle \ phi \ rightarrow (\ exists x \ psi)}$ é equivalente a (supondo que ), ${\ displaystyle \ exists x (\ phi \ rightarrow \ psi)}$${\ displaystyle \ existe x \ top}$

${\ displaystyle \ phi \ rightarrow (\ forall x \ psi)}$ é equivalente a . ${\ displaystyle \ forall x (\ phi \ rightarrow \ psi)}$

Exemplo

Suponha que , e sejam fórmulas livres de quantificador e nenhuma dessas fórmulas compartilhe qualquer variável livre. Considere a fórmula ${\ displaystyle \ phi}$${\ displaystyle \ psi}$${\ displaystyle \ rho}$

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

Ao aplicar recursivamente as regras começando nas subfórmulas mais internas, a seguinte sequência de fórmulas logicamente equivalentes pode ser obtida:

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

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

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

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

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

${\ displaystyle \ forall x ((\ phi \ lor \ psi) \ rightarrow \ forall z \ rho)}$ ,

${\ displaystyle \ forall x (\ forall z ((\ phi \ lor \ psi) \ rightarrow \ rho))}$ ,

${\ displaystyle \ 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 o consequente antes do antecedente no exemplo acima, a forma prenex

${\ displaystyle \ forall z \ forall x ((\ phi \ lor \ psi) \ rightarrow \ rho)}$

pode ser obtido:

${\ displaystyle \ forall z ((\ phi \ lor \ exists x \ psi) \ rightarrow \ rho)}$

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

${\ displaystyle \ forall z (\ forall x ((\ phi \ lor \ psi) \ rightarrow \ rho))}$ ,

${\ displaystyle \ forall z \ forall x ((\ phi \ lor \ psi) \ rightarrow \ rho)}$ .

Lógica intuicionista

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

A interpretação BHK ilustra por que algumas fórmulas não têm forma prenex intuicionisticamente equivalente. Nesta interpretação, uma prova de

${\ displaystyle (\ exists x \ phi) \ rightarrow \ exists y \ psi \ qquad (1)}$

é uma função que, dado um x concreto e uma prova de , produz um y concreto e uma prova de . Nesse caso, é permitido que o valor de y seja calculado a partir do valor fornecido de x . Uma prova de ${\ displaystyle \ phi (x)}$${\ displaystyle \ psi (y)}$

${\ displaystyle \ exists y (\ exists x \ phi \ rightarrow \ psi), \ qquad (2)}$

por outro lado, produz um único valor concreto de y e uma função que converte qualquer prova de em uma prova de . Se cada x satisfatório pode ser usado para construir um y satisfatório, mas nenhum y pode ser construído sem o conhecimento de tal x, então a fórmula (1) não será equivalente à fórmula (2). ${\ displaystyle \ existe x \ phi}$${\ displaystyle \ psi (y)}$${\ displaystyle \ phi}$${\ displaystyle \ psi}$

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

(1) implica , ${\ displaystyle \ forall x (\ phi \ lor \ psi)}$${\ displaystyle (\ forall x \ phi) \ lor \ psi}$

(2) implica , ${\ displaystyle \ forall x (\ phi \ lor \ psi)}$${\ displaystyle \ phi \ lor (\ forall x \ psi)}$

(3) implica , ${\ displaystyle (\ forall x \ phi) \ rightarrow \ psi}$${\ displaystyle \ exists x (\ phi \ rightarrow \ psi)}$

(4) implica , ${\ displaystyle \ phi \ rightarrow (\ exists x \ psi)}$${\ displaystyle \ exists x (\ phi \ rightarrow \ psi)}$

(5) implica , ${\ displaystyle \ lnot \ forall x \ phi}$${\ displaystyle \ existing x \ lnot \ phi}$

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

Uso de formulário prenex

Alguns cálculos de prova lidarão apenas com uma teoria cujas fórmulas são escritas na forma normal prenex. O conceito é essencial para desenvolver a hierarquia aritmética e a hierarquia analítica .

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

Axiomas de Tarski para a geometria é um sistema lógico cujas sentenças podem todos ser escrito em forma universal-existencial , um caso especial da forma normal prenex que tem todo o quantificador universal precede qualquer quantificador existencial , de modo que todas as sentenças pode ser reescrita na forma , onde é uma frase que não contém nenhum quantificador. Este fato permitiu a Tarski provar que a geometria euclidiana é decidível . ${\ displaystyle \ forall u}$ ${\ displaystyle \ forall v}$ ${\ displaystyle \ ldots}$ ${\ displaystyle \ existe um}$ ${\ displaystyle \ existe b}$ ${\ displaystyle \ phi}$${\ displaystyle \ phi}$

Veja também

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

Notas

Referências

• Richard L. Epstein (18 de dezembro de 2011). Lógica Matemática Clássica: Os Fundamentos Semânticos da Lógica . Princeton University Press. pp. 108–. ISBN   978-1-4008-4155-4 .
• Peter B. Andrews (17 de abril de 2013). Uma introdução à lógica matemática e à teoria dos tipos: para a verdade através da prova . Springer Science & Business Media. pp. 111–. ISBN   978-94-015-9934-4 .
• Elliott Mendelson (1 de junho de 1997). Introdução à lógica matemática, quarta edição . CRC Press. pp. 109–. ISBN   978-0-412-80830-2 .
• Hinman, P. (2005), Fundamentals of Mathematical Logic , AK Peters , ISBN   978-1-56881-262-5