Normalização de provas na dedução natural
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[editar | editar código-fonte]
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[editar | editar código-fonte]
Sendo Σn uma árvore de prova qualquer da dedução natural.
ß - E[editar | editar código-fonte]
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[editar | editar código-fonte]
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[editar | editar código-fonte]
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[editar | editar código-fonte]
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[editar | editar código-fonte]
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[editar | editar código-fonte]
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[editar | editar código-fonte]
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[editar | editar código-fonte]
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)[editar | editar código-fonte]
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[editar | editar código-fonte]
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[editar | editar código-fonte]
Qualquer que seja a ordem da aplicação das regras de redução irá levar a uma forma normal da árvore de dedução.