Normalização de provas na dedução natural é o processo de eliminar possíveis redundâncias existentes numa árvore de prova criada a partir da Dedução natural, assim obtendo a dedução mais simples possível, o que chamamos de "prova direta" ou "prova normal".
Introdução
Uma prova (ou dedução) de um argumento pode estar desnecessariamente longa, dada a existência de redundâncias em sua árvore sintática. Existem dois tipos de redundâncias:
Redundâncias do tipo ß: Uma regra de eliminação está sendo aplicada logo após a aplicação de uma regra de introdução do mesmo operador.
Redundâncias do tipo η: Uma regra de introdução está sendo aplicada logo após a aplicação de uma regra de eliminação do mesmo operador.
Tipos de redundância
Sendo Σn uma árvore de prova qualquer da dedução natural.
ß - E
Ocorrem quando usa-se a regra de eliminação do E logo após a regra de introdução do mesmo.
Σ1 Σ2 A B
AB A Σ3
No exemplo acima, temos que a partir das árvores Σ1 chegamos em A e B, respectivamente. Com isso, usamos a introdução do E, e logo após a exclusão do mesmo para chegarmos novamente a A, assim criando uma redundância do tipo ß.
Então, utilizamos a normalização do tipo ß para o operador E, que consiste em retirar da árvore sintática a introdução e a exclusão do E, eliminando assim a redundância, obtendo a seguinte prova normal:
Σ1 A Σ3
ß - OU
Ocorrem quando usa-se a regra de eliminação do OU logo após a regra de introdução do mesmo.
Σ1 A A B
[A] [B] Σ2 Σ3 C C
C Σ4
No exemplo acima, chegamos em A a partir de Σ1 e aplicamos a regra de introdução do OU para chegarmos a A v B. Logo após é utilizada a regra de exclusão do OU para chegarmos em C, criando assim uma redundância do tipo ß.
Então, utilizamos a normalização do tipo ß para o operador OU, que consiste em retirar da árvore sintática a introdução e a exclusão do OU, assim eliminando a redundância e obtendo a seguinte prova normal: Σ1 A Σ2 C Σ4
ß - Implica
Ocorrem quando usa-se a regra de eliminação do Implica logo após o a regra de introdução do mesmo.
[A] Σ1 Σ2 B
A A → B
B Σ3
No exemplo acima, temos a introdução de A->B, a dedução de A a partir da árvore Σ2, e a eliminação da implicação A->B, criando assim uma redundância do tipo ß.
Então, utilizamos a normalização do tipo ß para o operador Implica. Como já tínhamos A a partir de Σ2, e chegamos a partir de A em B a partir de Σ1, a hipótese de A é desnecessária. Então usamos a normalização tipo ß para o operador Implica, eliminando essa redundância e obtendo a seguinte prova normal:
Σ2 A Σ1 B Σ3
η - E
Ocorrem quando usa-se a regra de introdução do E logo após a regra de eliminação do mesmo.
Σ1 Σ1 A1 A2 A1 A2
A1 A2
A1 A2 Σ2
No exemplo acima, vemos que A1 e A2 foram extraídos de A1 ^ A2 por meio de uma eliminação para, a partir de ambos, concluir-se Σ2. Não era necessário ocorrer nenhuma das eliminações, já que Σ2 foi provado a partir da veracidade simultânea de A1 e A2, ou seja, A1 ^ A2. Logo, ocorreu a eliminação do E logo após a sua introdução, gerando assim uma redundância. Então aplicamos a normalização η do operador E, chegando assim a seguinte prova normal:
Σ1 A1 A2 Σ2
η - Ou
Ocorrem quando usa-se a regra de introdução do Ou logo após a regra de eliminação do mesmo.
Σ1 A1 A2
[A1] [A2] A1 A2 A1 A2
A1 A2 Σ2
No exemplo acima eliminamos o OU (A1 v A2) para chegarmos a [A1] e [A2], para então introduzirmos o mesmo A1 v A2 na hora de fecharmos a hipótese, gerando assim uma redundância. Então, temos que executar uma normalização do tipo η do operador Ou, para chegarmos a seguinte prova normal:
Σ1 A1 A2 Σ2
η - Implica
Ocorrem quando usa-se a regra de introdução do Implica logo após a regra de eliminação do mesmo.
Σ1 [A] A → B
B
A → B Σ2
No exemplo acima, B é extraído de A → B com o uso da suposição de A, para depois incluirmos A → B novamente e chegarmos a Σ2. Ou seja, geramos uma redundância, visto que o Implica foi eliminado desnecessariamente, pois a partir dessa eliminação chegamos em B, que foi usado para introduzirmos novamente o Implica. Então, usamos a normalização do tipo η do Implica, para chegarmos a seguinte forma normal:
Σ1 A → B Σ2
Fórmula máxima
Seja Σ uma árvore de prova que contêm redundâncias do tipo ß. Assim sendo, Σ contêm uma fórmula φ que é: - O resultado de uma regra de introdução - A maior premissa de uma regra de eliminação A φ damos o nome de fórmula máxima.
Procedimento de normalização de provas
Seja Σ uma árvore de prova que não está na forma normal (ou seja, contêm redundâncias), então:
1)Escolha a maior fórmula máxima e aplique a normalização do tipo ß correspondente ali.
2)Enquanto houver fórmulas máximas, continue executando o passo 1. O resultado poderá conter redundâncias do tipo η. Nesse caso, basta aplicar as normalizações do tipo η para chegar-se à forma normal.
Teorema da existência da forma normal (ou teorema da normalização fraca)
O procedimento de normalização termina produzindo uma prova na forma normal. Ou seja, para quaisquer Γ e φ, se Γ ╞ φ, então existe uma dedução normal de φ a partir de Γ.
Teorema da unicidade da forma normal
A forma normal de uma prova Σ, que possui apenas redundâncias dos operadores de implicação e conjunção, é única, independente da ordem de aplicação das regras de redução.
Teorema da normalização forte
Qualquer que seja a ordem da aplicação das regras de redução irá levar a uma forma normal da árvore de dedução.
Ligações externas http://cin.ufpe.br/~mlogica/livros/Apostila%20-%20Normalizacao%20de%20Provas%20na%20Deducao%20Natural.pdf
Categoria:Lógica matemática