Teorema de Herbrand
Em lógica matemática, o teorema de Herbrand é um resultado básico de Jacques Herbrand (1930). Ele essencialmente permite um tipo de redução da lógica de primeira ordem para a lógica proposicional. Embora originalmente Herbrand tenha provado seu teorema para fórmulas arbitrárias da lógica de primeira ordem, a versão mais simples, mostrada aqui, que é restrita a fórmulas em forma normal prenex contendo apenas quantificadores existenciais, tornou-se mais popular.
Sendo
a fórmula de primeira ordem com
- quantificadores livres.
Então
é válido se, e somente se, existe uma sequência finita de termos :, com
- e ,
de tal forma que
é válido. Se isto é válido,
é chamado de disjunção de Herbrand para
- .
Informalmente: uma fórmula , em forma prenex contendo quantificadores existenciais só é demonstrável (válida) em lógica de primeira ordem se e somente se uma disjunção composta de instâncias de substituição da sub-fórmula de quantificadores livres de A é uma Tautologia (lógica) (proposicionalmente derivável).
A restrição às fórmulas em forma prenex contendo somente quantificadores existenciais não limita a generalidade do teorema, porque as fórmulas podem ser convertidas para a forma prenex e seus quantificadores universais podem ser removidos.
Esboço da Prova
Uma prova da direção não-trivial do teorema pode ser construída segundo os seguintes passos:
- Se a fórmula é válida, então por completude de cálculo de sequentes,[1] que segue a partir do teorema da eliminação de corte de Gentzen, existe uma prova livre de corte de .
- Partindo de cima para baixo, remova as inferências que introduzem quantificadores existenciais.
- Remova as inferências de contração sobre fórmulas quantificadas previamente existentes, uma vez que as fórmulas (agora com termos substituídos por variáveis previamente quantificadas) não podem mais ser idênticas após a remoção das inferências quantificador.
- A remoção das contrações acumula todas as instâncias de substituição relevantes de no lado direito da seqüente, resultando assim em uma prova de , da qual a disjunção Herbrand podem ser obtida.
No entanto, o cálculo de sequentes e a eliminação de corte não eram conhecidos na época do teorema de Herbrand, e Herbrand teve que provar seu teorema de uma forma mais complicada.
Generalizações do Teorema de Herbrand
- Teorema de Herbrand foi estendido para lógicas de ordem superior arbitrárias usando a provas de expansão por árvore. A representação de profundidade de provas de expansão por árvore correspondem a disjunções Herbrand, quando restrita à lógica de primeira ordem.
- Disjunções de Herbrand e provas por expansão de árvore foram estendidas com uma noção de corte. Devido à complexidade da eliminação por corte, disjunções de Herbrand com cortes podem ser, de maneira não elementar, menores do que disjunções de Herbrand padrões.
- Disjunções de Herbrand foram generalizados para sequentes de Herbrand, permitindo que o teorema de Herbrand seja enunciado para sequentes: "um sequente skolemizado é derivável sse ele é um sequente de Herbrand".
Aplicações do teorema de Herbrand
- Teorema de Herbrand fornece a base teórica para as técnicas de prova automática de teorema na lógica de primeira ordem, como o Algoritmo de Davis-Putnam.
- A extração de sequentes de Herbrand das provas em cálculos de sequentes tem sido usada para obter e representar de forma compacta a informação essencial de uma prova formal.[2]
Ver também
- Universo de Herbrand
- Teorema da compacidade
Notas e referências
Referências
- Buss, Samuel R. (1995), «On Herbrand's Theorem», in: Maurice, Daniel; Leivant, Raphaël, Logic and Computational Complexity, ISBN 978-3-540-60178-4, Lecture Notes in Computer Science, Berlin, New York: Springer-Verlag, pp. 195–209 .
Portal da matemática