Estructura de Herbrand

El universo de Herbrand sirve como universo en una estructura de Herbrand .

Dejar${\displaystyle L^{\sigma }}$, ser un lenguaje de primer orden con el vocabulario

• símbolos constantes:${\displaystyle c}$
• símbolos de función:${\displaystyle f(\cdot ),\,g(\cdot )}$

Luego, el universo de Herbrand${\displaystyle H}$de${\displaystyle L^{\sigma }}$(o de${\displaystyle \sigma }$) es

${\displaystyle H=\{c,f(c),g(c),f(f(c)),f(g(c)),g(f(c)),g(g(c)),\dots \}}$

Los símbolos de relación no son relevantes para un universo de Herbrand ya que las fórmulas que involucran solo relaciones no corresponden a elementos del universo. ^{[ 2 ]}

Dejar${\displaystyle S}$ser una estructura , con vocabulario${\displaystyle \sigma }$y universo${\displaystyle U}$. Dejar${\displaystyle W}$ser el conjunto de todos los términos sobre${\displaystyle \sigma }$y${\displaystyle W_{0}}$sea ​​el subconjunto de todos los términos sin variables.${\displaystyle S}$Se dice que es una estructura Herbrand si

1. ${\displaystyle U=W_{0}}$
2. ${\displaystyle f^{S}(t_{1},\dots ,t_{n})=f(t_{1},\dots ,t_{n})}$por cada${\displaystyle n}$-ario símbolo de función${\displaystyle f\in \sigma }$y${\displaystyle t_{1},\dots ,t_{n}\in W_{0}}$
3. ${\displaystyle c^{S}=c}$para cada constante${\displaystyle c}$en${\displaystyle \sigma }$

1. ${\displaystyle U}$es el universo de Herbrand de${\displaystyle \sigma }$.
2. Una estructura de Herbrand que es un modelo de una teoría${\displaystyle T}$se denomina modelo Herbrand de${\displaystyle T}$.

Para un símbolo constante${\displaystyle c}$y un símbolo de función unaria${\displaystyle f(\,\cdot \,)}$Tenemos la siguiente interpretación:

• ${\displaystyle U=\{c,fc,ffc,fffc,\dots \}}$
• ${\displaystyle fc\mapsto fc,ffc\mapsto ffc,\dots }$
• ${\displaystyle c\mapsto c}$

Una base Herbrand${\displaystyle {\mathcal {B}}_{H}}$Una estructura de Herbrand es el conjunto de todas las fórmulas atómicas cuyos términos de argumento son elementos del universo de Herbrand.

Para un símbolo de relación binaria${\displaystyle R}$, obtenemos con los términos anteriores:

${\displaystyle {\mathcal {B}}_{H}=\{R(c,c),R(fc,c),R(c,fc),R(fc,fc),R(ffc,c),\dots \}}$