# 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
    $(\exists y_{1},\ldots ,y_{n})F(y_{1},\ldots ,y_{n})$
a fórmula de primeira ordem com
    $F(y_{1},\ldots ,y_{n})$ quantificadores livres.
Então
    $(\exists y_{1},\ldots ,y_{n})F(y_{1},\ldots ,y_{n})$
é válido se, e somente se, existe uma sequência finita de termos :$t_{ij}$, com
    $1\leq i\leq k$ e $1\leq j\leq n$,
de tal forma que
    $F(t_{11},\ldots ,t_{1n})\vee \ldots \vee F(t_{k1},\ldots ,t_{kn})$
é válido. Se isto é válido,
    $F(t_{11},\ldots ,t_{1n})\vee \ldots \vee F(t_{k1},\ldots ,t_{kn})$
é chamado de disjunção de Herbrand para
    $(\exists y_{1},\ldots ,y_{n})F(y_{1},\ldots ,y_{n})$.
Informalmente: uma fórmula $A$, 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 $(\exists y_{1},\ldots ,y_{n})F(y_{1},\ldots ,y_{n})$ é válida, então por completude de cálculo de sequentes, que segue a partir do teorema da eliminação de corte de Gentzen, existe uma prova livre de corte de $\vdash (\exists y_{1},\ldots ,y_{n})F(y_{1},\ldots ,y_{n})$.
* 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 $F(y_{1},\ldots ,y_{n})$ no lado direito da seqüente, resultando assim em uma prova de $\vdash F(t_{11},\ldots ,t_{1n}),\ldots ,F(t_{k1},\ldots ,t_{kn})$, 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.