Herbrand Universe (First-Order Logic)

first-order-logic

Definition

Herbrand Universe (First-Order Logic)

Let $(\mathcal{F},\mathcal{P})$ be a signature. The Herbrand universe $\mathcal{H}$ is the set of all ground terms over $\mathcal{F}$. If $\mathcal{F}$ contains no constant of arity $0$, a fresh constant is added to ensure $\mathcal{H}\ne \varnothing$.

Examples

Example

Let $\mathcal{F}=\{\text{zero}/0,\text{succ}/1\}$. Then

$$\mathcal{H}=\{\text{zero},\text{succ}(\text{zero}),\text{succ}(\text{succ}(\text{zero})),\dots \}$$