# 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.
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:

### ß - OU

Ocorrem quando usa-se a regra de eliminação do OU logo após a regra de introdução do mesmo.
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:

### ß - Implica

Ocorrem quando usa-se a regra de eliminação do Implica logo após o a regra de introdução do mesmo.
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:

### η - E

Ocorrem quando usa-se a regra de introdução do E logo após a regra de eliminação do mesmo.
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:

### η - Ou

Ocorrem quando usa-se a regra de introdução do Ou logo após a regra de eliminação do mesmo.
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:

### η - Implica

Ocorrem quando usa-se a regra de introdução do Implica logo após a regra de eliminação do mesmo.
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:

## Fórmula máxima

Seja Σ uma árvore de prova que contêm redundâncias do tipo ß. Assim sendo, Σ contêm uma fórmula φ que é:
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.