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 ${\displaystyle F}$ uma fórmula na linguagem da Lógica de primeira ordem. Podemos assumir que ${\displaystyle 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, ${\displaystyle F}$ pode ser reescrita para assegurar essas condições, de modo que o resultado é uma fórmula equivalente).

A Herbrandização de ${\displaystyle F}$ é obtida da seguinte maneira:

• Primeiro, substitua qualquer variável livre em ${\displaystyle 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 ${\displaystyle v}$ por um símbolo de função, ${\displaystyle f_{v}(x_{1},\dots ,x_{k})}$, onde ${\displaystyle x_{1},\dots ,x_{k}}$ são as variáveis que continuam quantificadas, e cujos quantificadores dominam ${\displaystyle v}$.

Exemplo

Considere a fórmula ${\displaystyle 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 ${\displaystyle y,z}$ são as que consideramos para o segundo passo, então apagamos os quantificadores ${\displaystyle \forall y}$ e ${\displaystyle \exists z}$. Finalmente, substituímos ${\displaystyle y}$ por um símbolo de constante ${\displaystyle c_{y}}$ (pois não há outros quantificadores dominando ${\displaystyle y}$), e substituímos ${\displaystyle z}$ por uma função, ${\displaystyle f_{z}(x)}$:

${\displaystyle 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:

${\displaystyle 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.

Ver também

• Skolemização
• Lógica de primeira ordem