Mostrar código-fonte de 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==


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
 -----------  
    A<math>\land</math>B                                    
    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 <math>\lor</math> 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 <math>\land</math> A2          A1 <math>\land</math> A2
 ---------       ---------
   A1               A2                  
 ------------------------
         A1 <math>\land</math> 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 <math>\land</math> 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 <math>\lor</math> A2
  ------------
  [A1]     [A2]          
 A1 <math>\lor</math> A2  A1 <math>\lor</math> A2                       
 ------------------                            
     A1 <math>\lor</math> 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 <math>\lor</math> 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]]