Herbrandização
# Herbrandização

A Herbrandização de uma fórmula lógica (denominação em homenagem a Jacques Herbrand) é um construção que é dual à Skolemização de uma fórmula. Thoralf Skolem tinha considerado a Skolemização de fórmulas na Forma normal prenex como parte da prova do Teorema de Löwenheim–Skolem (Skolem 1920). Herbrand trabalhou com essa noção dual de Herbrandização, generalizada para se aplicar a fórmulas não-prenex também, com o objetivo de provar o Teorema de Herbrand (Herbrand 1930).
A fórmula resultante não é necessariamente equivalente à original. Assim como acontece na Skolemização, que somente preserva a satisfatibilidade, a Herbrandização sendo uma dual da Skolemização, preserva a validade: a fórmula resultante é válida se e somente se a original for.
Seja $F$ uma fórmula na linguagem da Lógica de primeira ordem. Podemos assumir que $F$ não contém nenhuma variável que está ligada a duas ocorrências de quantificadores diferentes, e que nenhuma variável ocorre livre e ligada. (Ou seja, $F$ pode ser reescrita para assegurar essas condições, de modo que o resultado é uma fórmula equivalente).
A Herbrandização de $F$ é obtida da seguinte maneira:
* Primeiro, substitua qualquer variável livre em $F$ por símbolos de constante;
* Depois, remova todos os quantificadores nas variáveis que (1) sejam quantificadas universalmente e que estejam dentro do escopo de uma quantidade par de símbolos de negação, ou (2) que sejam quantificadas existencialmente, e com estejam dentro do escopo de uma quantidade impar de símbolos de negação;
* Finalmente, substitua cada variável $v$ por um símbolo de função, $f_{v}(x_{1},\dots ,x_{k})$, onde $x_{1},\dots ,x_{k}$ são as variáveis que continuam quantificadas, e cujos quantificadores dominam $v$.

## Exemplo

Considere a fórmula $F:=\forall y\exists x[R(y,x)\wedge \neg \exists zS(x,z)]$. Não há variáveis livres para substituir. As variáveis $y,z$ são as que consideramos para o segundo passo, então apagamos os quantificadores $\forall y$ e $\exists z$. Finalmente, substituímos $y$ por um símbolo de constante $c_{y}$ (pois não há outros quantificadores dominando $y$), e substituímos $z$ por uma função, $f_{z}(x)$:
    $F^{H}=\exists x[R(c_{y},x)\wedge \neg S(x,f_{z}(x))].$
A Skolemização de uma fórmula é obtida de modo parecido, exceto que no segundo passo, poderíamos deletar os quantificadores das variáveis que tanto estivesse com quantificadores existenciais e número par de negação, ou com quantificadores universais e número impar de negação.
Considerando a mesma fórmula anterior, sua Skolemização ficaria:
    $F^{S}=\forall y[R(y,f_{x}(y))\wedge \neg \exists zS(f_{x}(y),z)].$
Para entende o significado dessas construções, veja Teorema de Herbrand ou o Teorema de Löwenheim–Skolem.