Teorema de Herbrand
Origem: Wikipédia, a enciclopédia livre.
Em lógica matemática, o teorema de Herbrand é um resultado básico de Jacques Herbrand. Ele essencialmente declara que na lógica de primeira ordem formal, toda regra para os quantificadores (
) podem ser permutada até o início de uma demonstração.
Formalmente: Numa lógica predicada sem igualdade, uma formula A na forma prenex (todos os quantificadores antes da formula) é apta a demonstração se e somente se uma sequência S abrangendo as instancias substituidas das meta-formulas de A livres de quantificadores é proposicionalmente derivavel, e A só pode ser obtida de S por regras estruturais e regras de quantificadores.
