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:=\mathrm{\forall }y\mathrm{\exists }x[R(y,x)\wedge \mathrm{\neg }\mathrm{\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 $\mathrm{\forall }y$ e $\mathrm{\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=\mathrm{\exists }x[R(c_y,x)\wedge \mathrm{\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=\mathrm{\forall }y[R(y,f_x(y))\wedge \mathrm{\neg }\mathrm{\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