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

${\displaystyle (\exists y_{1},\ldots ,y_{n})F(y_{1},\ldots ,y_{n})}$

a fórmula de primeira ordem com

${\displaystyle F(y_{1},\ldots ,y_{n})}$ quantificadores livres.

Então

${\displaystyle (\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 :${\displaystyle t_{ij}}$, com

${\displaystyle 1\leq i\leq k}$ e ${\displaystyle 1\leq j\leq n}$,

de tal forma que

${\displaystyle F(t_{11},\ldots ,t_{1n})\vee \ldots \vee F(t_{k1},\ldots ,t_{kn})}$

é válido. Se isto é válido,

${\displaystyle F(t_{11},\ldots ,t_{1n})\vee \ldots \vee F(t_{k1},\ldots ,t_{kn})}$

é chamado de disjunção de Herbrand para

${\displaystyle (\exists y_{1},\ldots ,y_{n})F(y_{1},\ldots ,y_{n})}$.

Informalmente: uma fórmula ${\displaystyle 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.

Uma prova da direção não-trivial do teorema pode ser construída segundo os seguintes passos:

1. Se a fórmula ${\displaystyle (\exists y_{1},\ldots ,y_{n})F(y_{1},\ldots ,y_{n})}$ é 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 ${\displaystyle \vdash (\exists y_{1},\ldots ,y_{n})F(y_{1},\ldots ,y_{n})}$.
2. Partindo de cima para baixo, remova as inferências que introduzem quantificadores existenciais.
3. 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.
4. A remoção das contrações acumula todas as instâncias de substituição relevantes de ${\displaystyle F(y_{1},\ldots ,y_{n})}$ no lado direito da seqüente, resultando assim em uma prova de ${\displaystyle \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.

• 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".

• 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]

• Universo de Herbrand
• Teorema da compacidade

Notas e 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