El conjunto de todos los términos ground (sin variables) que se pueden formar a partir de los símbolos de constantes y funciones de un lenguaje de primer orden.

Principio

Construir la menor álgebra de términos cerrada bajo las constantes y las funciones de la firma; no se permiten variables, por lo que la aplicación iterada de funciones sobre términos ya formados genera el conjunto.

Demostración

Con firma que contiene la constante a y la función unaria f, el universo de Herbrand es {a, f(a), f(f(a)), ...}, a menudo infinito, obtenido aplicando f repetidamente a a.

Aplicación incorrecta

Confundir el universo de Herbrand con un dominio semántico interpretado o asumir que es finito cuando la firma tiene símbolos de función que generan infinitos términos.

Consecuencia

Proporciona un dominio puramente sintáctico para construir instancias ground de fórmulas y para definir interpretaciones y modelos de Herbrand usados en demostración automática y programación lógica.

Inversión

En lugar del cierre en términos ground, considerar el conjunto de términos con variables o un dominio interpretado — el enfoque cambia de la construcción sintáctica de términos a la interpretación semántica o a patrones con variables.

Límite

Incluye solo términos ground formados con las constantes y funciones del lenguaje; excluye variables, símbolos de predicado, metatérminos y símbolos externos a la firma, y por sí solo no asigna valores de verdad.

Tensión semántica

Tensión entre el universo de Herbrand como álgebra de términos puramente sintáctica y la noción de dominio en teoría de modelos; ambos usan 'dominio' pero designan cosas distintas.

Síntesis

El universo de Herbrand es el universo sintáctico de términos ground generado por las constantes y funciones de la firma; sirve como base para groundear fórmulas, construir la base de Herbrand y conectar métodos de prueba sintácticos con razonamiento semántico.