Herbrand Interpretation (First-Order Logic)

first-order-logic

Definition

Herbrand Interpretation (First-Order Logic)

A Herbrand interpretation is an interpretation whose domain is the Herbrand universe $\mathcal{H}$ and where each ground term $t$ is interpreted as itself:

$$t^{\mathcal{I}}=t$$

A Herbrand interpretation is fully determined by which ground atoms it makes true.

Examples

Example

Let

$$\mathcal{F}=\{\text{zero}/0,\text{succ}/1\},\mathcal{P}=\{\text{Even}/1\}$$

The Herbrand universe is

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

One Herbrand interpretation makes $\text{Even}(\text{zero})$ and $\text{Even}(\text{succ}(\text{succ}(\text{zero})))$ true but $\text{Even}(\text{succ}(\text{zero}))$ false — encoding that $0$ and $2$ are even, $1$ is not.