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 uma fórmula na linguagem da Lógica de primeira ordem. Podemos assumir que 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, pode ser reescrita para assegurar essas condições, de modo que o resultado é uma fórmula equivalente).
A Herbrandização de é obtida da seguinte maneira:
- Primeiro, substitua qualquer variável livre em 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 por um símbolo de função, , onde são as variáveis que continuam quantificadas, e cujos quantificadores dominam .
Exemplo[editar | editar código-fonte]
Considere a fórmula . Não há variáveis livres para substituir. As variáveis são as que consideramos para o segundo passo, então apagamos os quantificadores e . Finalmente, substituímos por um símbolo de constante (pois não há outros quantificadores dominando ), e substituímos por uma função, :
![{\displaystyle F:=\forall y\exists x[R(y,x)\wedge \neg \exists zS(x,z)]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7d3321fbf9a9a846d204f2c88df22a227925a749)
![{\displaystyle F^{H}=\exists x[R(c_{y},x)\wedge \neg S(x,f_{z}(x))].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0ba6db31371a466dd2548b6b042f8746ca23ee03)
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)].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/724fad0f44998a4ee22f7599858d4bfcf30577f6)
Para entende o significado dessas construções, veja Teorema de Herbrand ou o Teorema de Löwenheim–Skolem.