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 

         
  
    
      
        ∀
        
          x
          
            1
          
        
        .
        .
        .
        ∀
        
          x
          
            n
          
        
        S
      
    
    {\displaystyle \forall x_{1}...\forall x_{n}S}

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

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

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

As cláusulas (disjunções de literais) obtidas daquelas de S {\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 S {\displaystyle S} e termos de H {\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 S = ¬ p ( X , Y ) ∨ q ( X , f ( X ) ) , ¬ p ( X , Y ) ∨ q ( X , g ( Y ) ) {\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 S {\displaystyle S} , seja então H 0 = a {\displaystyle H_{0}={a}} . Assim 


  
    
      
        
          H
          
            1
          
        
        =
        
          H
          
            0
          
        
        ∪
        {
        f
        (
        a
        )
        ,
        g
        (
        a
        )
        }
      
    
    {\displaystyle H_{1}=H_{0}\cup \{f(a),g(a)\}}
  


  
    
      
        
          H
          
            2
          
        
        =
        
          H
          
            1
          
        
        ∪
        {
        f
        (
        f
        (
        a
        )
        )
        ,
        f
        (
        g
        (
        a
        )
        )
        ,
        g
        (
        f
        (
        a
        )
        )
        ,
        g
        (
        g
        (
        a
        )
        )
        }
      
    
    {\displaystyle H_{2}=H_{1}\cup \{f(f(a)),f(g(a)),g(f(a)),g(g(a))\}}
  


  
    
      
        
          H
          
            3
          
        
        =
        
          H
          
            2
          
        
        ∪
        {
        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 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
        )
        )
        )
        }
      
    
    {\displaystyle g(g(f(a))),g(g(g(a)))\}}
  


  
    
      
        .
        .
        .
        .
        .
        .
      
    
    {\displaystyle ......}
  


  
    
      
        
          H
          
            ∞
          
        
        =
        {
        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 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))),}
  

        
  
    
      
        f
        (
        g
        (
        g
        (
        a
        )
        )
        )
        ,
        g
        (
        f
        (
        f
        (
        a
        )
        )
        )
        ,
        g
        (
        f
        (
        g
        (
        a
        )
        )
        )
        ,
        g
        (
        g
        (
        f
        (
        a
        )
        )
        )
        ,
        g
        (
        g
        (
        g
        (
        a
        )
        )
        )
        ,
        .
        .
        .
        }
      
    
    {\displaystyle 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 ) ∨ q ( X ) , r ( Z ) , ¬ s ( Y ) ∨ t ( W ) } {\displaystyle S=\{p(X)\lor q(X),r(Z),\neg s(Y)\lor t(W)\}}

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

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

Ver também

Referências

  • Herbrand Universe (MathWorld)
  • Apostila online