Universo de Herbrand

Na lógica matemática, dada uma linguagem formal com um conjunto de símbolos (símbolos de constantes e símbolos funcionais), o universo de Herbrand define recursivamente o conjunto de todos os termos que podem ser compostos aplicando uma composição funcional a partir de símbolos básicos.

Foi assim denominada em homenagem a Jacques Herbrand.

Dada uma linguagem de primeira ordem L, seu universo de Herbrand é definido pelo conjunto de todas as cláusulas básicas que podem ser construídas a partir dos símbolos de L. Levando em conta a definição de termo básico, podemos observar que os símbolos que aparecem em um universo de Herbrand são funtores e constantes de L.

Considere uma fórmula da lógica de primeira ordem ${\displaystyle \Phi }$ na forma skolemizada

         ${\displaystyle \forall x_{1}...\forall x_{n}S}$

Então o universo de Herbrand ${\displaystyle H}$ de ${\displaystyle S}$ é definido pelas seguintes regras.

1. Todas as constantes de ${\displaystyle S}$ pertencem a ${\displaystyle H}$. Se não existem constantes em ${\displaystyle S}$, então ${\displaystyle H}$ contém uma constante arbitrária ${\displaystyle c}$.

2. Se ${\displaystyle t_{1}\in H,...,t_{n}\in H}$, e uma função ${\displaystyle n}$-ária ${\displaystyle f}$ ocorre em ${\displaystyle S}$, então ${\displaystyle f(t_{1},...,t_{n})\in H}$.

As cláusulas (disjunções de literais) obtidas daquelas de ${\displaystyle S}$ substituindo todas as variáveis por elementos do universo de Herbrand são chamadas cláusulas básicas, com definições similares para literais básicos e átomos básicos. O conjunto de todos os átomos básicos que pode ser formados a partir de símbolos predicados de ${\displaystyle S}$ e termos de ${\displaystyle H}$ é chamado de Base de Herbrand.

A geração consecutiva de elementos do universo de Herbrand e a verificação de insatisfatibilidade de elementos gerados podem ser diretamente implementadas em um programa de computador. Tendo em vista a completude da lógica de primeira ordem, esse programa é basicamente uma ferramenta para a demonstração automática de teoremas. Evidentemente, essa busca exaustiva é muito lenta para aplicações práticas.

Esse programa irá terminar a execução para todas as fórmulas insatisfatíveis e não terminará para fórmulas satisfatíveis, que basicamente mostra que o conjunto das fórmulas insatisfatíveis é recursivamente enumerável. Dado que a demonstrabilidade (ou, equivalentemente, a insatisfatibilidade) na lógica de primeira-ordem é recursivamente indecidível, esse conjunto não é recursivo.

Exemplo

1. Seja ${\displaystyle S={\neg p(X,Y)\lor q(X,f(X)),\neg p(X,Y)\lor q(X,g(Y))}}$

Desde que não existe constante em ${\displaystyle S}$, seja então ${\displaystyle H_{0}={a}}$. Assim

${\displaystyle H_{1}=H_{0}\cup \{f(a),g(a)\}}$
${\displaystyle H_{2}=H_{1}\cup \{f(f(a)),f(g(a)),g(f(a)),g(g(a))\}}$
${\displaystyle H_{3}=H_{2}\cup \{f(f(f(a))),f(f(g(a))),f(g(f(a))),f(g(g(a))),g(f(f(a))),g(f(g(a))),}$
            ${\displaystyle g(g(f(a))),g(g(g(a)))\}}$
${\displaystyle ......}$
${\displaystyle H_{\infty }=\{a,f(a),g(a),f(f(a)),f(g(a)),g(f(a)),g(g(a)),f(f(f(a))),f(f(g(a))),f(g(f(a))),}$
        ${\displaystyle f(g(g(a))),g(f(f(a))),g(f(g(a))),g(g(f(a))),g(g(g(a))),...\}}$

2. Seja ${\displaystyle S=\{p(X)\lor q(X),r(Z),\neg s(Y)\lor t(W)\}}$

Desde que não exista constante em ${\displaystyle S}$, seja então ${\displaystyle H_{0}={a}}$.

Desde que não exista símbolo funcional em ${\displaystyle S}$, ${\displaystyle H_{0}=H_{1}=H_{2}=...={a}}$

Ver também

• Base de Herbrand
• Skolemização

Referências

• Herbrand Universe (MathWorld)
• Apostila online