Universo de Herbrand

Predefinição:Sem notas Predefinição:Wikificação 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 $\mathrm{\Phi }$ na forma skolemizada

         $\mathrm{\forall }{x}_1...\mathrm{\forall }{x}_{n}S$

Então o universo de Herbrand $H$ de $S$ é definido pelas seguintes regras.

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

2. Se $t_1\in H,...,t_n\in H$, e uma função $n$-ária $f$ ocorre em $S$, então $f(t_1,...,t_n)\in H$.

As cláusulas (disjunções de literais) obtidas daquelas de $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 $S$ e termos de $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 $S=\mathrm{\neg }p(X,Y)\vee q(X,f(X)),\mathrm{\neg }p(X,Y)\vee q(X,g(Y))$

Desde que não existe constante em $S$, seja então $H_0=a$. Assim

$H_1=H_0\cup \{f(a),g(a)\}$
$H_2=H_1\cup \{f(f(a)),f(g(a)),g(f(a)),g(g(a))\}$
$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))),$
            $g(g(f(a))),g(g(g(a)))\}$
$......$
$H_{\mathrm{\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))),$
        $f(g(g(a))),g(f(f(a))),g(f(g(a))),g(g(f(a))),g(g(g(a))),...\}$

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

Desde que não exista constante em $S$, seja então $H_0=a$.

Desde que não exista símbolo funcional em $S$, $H_0=H_1=H_2=...=a$

Ver também

• Base de Herbrand
• Skolemização

Referências

• Herbrand Universe (MathWorld)
• Apostila online