Herbrand Structure (First-Order Logic)

first-order-logic

Definition

Herbrand Structure (First-Order Logic)

A Herbrand structure is a structure $\mathcal{M}=(\mathcal{D},\mathcal{I})$ where the domain $\mathcal{D}$ is the Herbrand universe $\mathcal{H}$ and each ground term is interpreted as itself:

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

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