Intuition about Herbrand Models.

Question

I'm having trouble understanding how Herbrand models work. I feel like there is a bigger picture to it which I'm not understanding.

Why does every satisfiable first order formula have a herbrand model at all ? Can I somehow construct a Herbrand model from a normal model ?

My book also says that : a formula is unsatisfiable iff the Herbrand expansion is unsatisfiable. The book I'm using "Mathematical Logic for computer science by Mordechai Ben-Ari" has all the proofs of the above but its not very intuitive to me.

Could somebody share their point of view?

Answer 1

In a nutshell, an Herbrand structure is a mathematical structure built with the syntactical stuff: terms are used as objects of the domain of the interpretation.

Herbrand's proof procedure is a way to reduce the compelxity of first-order logic to propositional calculus, replacing quantified formulas with clauses.

We consider a theory $T$ (a set of formulas) and we transform it in a set $S$ of clauses.

We use the constants of the theory (or an arbitrary one $a$, if no constant at all is used: this amounts to the assumption of "standard" FOL semantics about interpretations with non-empty domain) to build up the H-universe (the domain made of syntactical stuff) using the function symbols of the theory to generate all the terms.

Example: if the theory (in clause form) is $S = \{ P(a), ¬P(x) ∨ P(f(a)) \}$, the H-universe will be: $H = \{ a,f(a),f(f(a)), \ldots \}$.

If neither constants nor function symbols are used, e.g. $S = \{ P(x), ¬P(x) ∨ P(y) \}$, the H-universe will be $H = \{ a \}$.

Terms without variables ("closed" terms), like $a$ and $f(a)$ above, are called ground terms.

Having the domain $H$, we build the interpretation: constants are interpreted with themselves, and function are interpreted as mapping from ground terms to ground terms.

Predicates are interpreted through ground instances obtained from clauses replacing variables with ground terms.

Let $S = \{ P(x), ¬P(x) ∨ P(f(a)) \}$; again we have $H = \{ a,f(a),\ldots \}$. The ground instances for clause $P(x)$ are: $P(a), P(f(a)), \ldots$.

The key result is:

A set of clauses $S$ is unsatisfiable iff $S$ is false under all the H-interpretations.

The first part of the theorem is obvious: if a set of formulas is false under all interpretations, it will be false also under the subset of the H-interpretations.

The non-trivial part is proved using an auxiliary Lemma:

Given an interpretation $I$ over some domain $D$ that satisfy a set of clauses $S$, we cam build a corresponding H-interpretation $I_H$ that also satisfy $S$.

The H-interpretation $I_H$ is manufactured from the domain $D$ mapping ground terms $h_i \in H$ to elements $d_i \in D$ and using gound instances:

$P^{I_H}(h_1, \ldots h_n)=$ T(F) iff $P^I(d_1, \ldots, d_n)=$ T(F).

Having the Lemma above, the proof of the last part of H's theorem is straightforward: assume that the set of clauses $S$ is false under all H-interpretation and assume that $S$ is satisfiable (i.e. not unsatisfiable).

Then there is an interpretation $I$ with domain $D$ such that $S$ is true in $I$.

By the Lemma we can build an H-interpretation $I_H$ corresponding to $I$ such that $S$ is true under $I_H$.

But this contradicts the assumption that $S$ is false under all H-interpretations.

Conclusion: $S$ must be unsatisfiable.