Notes - Logic and Proof MT24, Herbrand's theorem
Herbrand’s theorem says that for closed Skolem formulas $F$, i.e. those in the form
\[F = \forall x_1 \cdots \forall x_n F^\ast\]$F$ is satisfiable if and only if it is satisfiable via a Herbrand model.
This is useful because it gives an effective semi-algorithm for unsatisfiability of first-order formulas, first by converting the formula to an equisatisfiable formula in Skolem form and then searching for (propositional) resolution refutation proofs using subsets of the Herbrand expansion.
However, it is only a semi-algorithm because there is no effective procedure for determining satisfiability. This can be proved by reduction to the Post correspondence problem ( [[Notes - Logic and Proof MT24, Decidability results for first-order logic]]U), but the intuitive reason why this is the case is because there might be existential and universal quantifiers in the formula. These mean that (in general) there is no finite witness of satisfiability; there are sentences which are only satisfied by infinite models.
Flashcards
Basic definitions
Suppose:
- $\sigma$ is a structure with at least one constant symbol
- $\mathcal H$ is a $\sigma$-structure
- We are considering first-order logic without equality
@Define what it means for $\mathcal H$ to be a Herbrand structure.
The following hold:
- The universe is the set $T _ \sigma$ of ground $\sigma$-terms (variable-less terms)
- For each constant symbol $c$ in $\sigma$, we have $c^\mathcal H = c$
- For each $k$-ary function symbol $f$ in $\sigma$ and $t _ 1, \ldots, t _ k \in T _ \sigma$, we have $f^\mathcal H(t _ 1, \ldots, t _ k) = f(t _ 1, \ldots, t _ k)$.
- (and each predicate $P^\mathcal H$ can still be arbitrary)
Suppose:
- $\mathcal H$ is a Herbrand structure
- $F$ is a formula
- $v$ is a valuation
- $t$ is a ground term
The ordinary translation lemma states that
\[\mathcal H, v \models F[t, x] \text{ iff } \mathcal H, v_{x \mapsto v[t]} \models F\]
@Prove that in a Herbrand structure, we actually have
\[\mathcal H, v \models F[t, x] \text{ iff } \mathcal H, v_{x \mapsto t} \models F\]
The key is to show that $v[t] = t$ for any term. We proceed by structural induction on terms.
The base case is that $t$ is a constant symbol $c$, then $c^\mathcal H = c$ by the definition of a Herbrand structure.
The induction step is that $t$ has the form $f(t _ 1, \ldots, t _ k)$ for a $k$-ary function symbol and ground terms $t _ 1, \ldots, t _ k$. Then
\[\begin{aligned} f(t_1, \ldots, t_k)^\mathcal H &= f^\mathcal H(t_1^\mathcal H, \ldots, t_k^\mathcal H) \\\\ &= f^\mathcal H(t_1, \ldots, t_k) \\\\ &= f(t_1, \ldots, t_k) \end{aligned}\]where in the second equality we used the inductive hypothesis.
Herbrand’s theorem
@State Herbrand’s theorem.
Suppose:
- $F = \forall x _ 1 \cdots \forall x _ n F^\ast$
- $F$ is a closed formula in Skolem form (i.e. it contains no free variables)
Then:
- $F$ is satisfiable iff it has a Herbrand model
@Prove Herbrand’s theorem, i.e. if:
- $F = \forall x _ 1 \cdots \forall x _ n F^\ast$
- $F$ is a closed formula in Skolem form (i.e. it contains no free variables)
then:
- $F$ is satisfiable iff it has a Herbrand model
Backward direction: Immediate, since the existence of a model implies that $F$ is satisfiable.
Forward direction: Suppose that $F$ is satisfied by a structure $\mathcal A$. We want to show that $F$ has a Herbrand model $\mathcal H$. To do this, we only need to define an interpretation of the predicate symbols.
For each $k$-ary predicate symbol $P$, let
\[(t_1, \ldots, t_k) \in P^\mathcal H\]if and only if
\[\mathcal A \models P(t_1, \ldots, t_k)\]We aim to show that now $\mathcal A$ and $\mathcal H$ agree on all closed formulas $G = \forall y _ 1 \cdots \forall y _ k G^\ast$.
Induct on the number of quantifiers $k$. If $k = 0$, then $G$ must be a boolean combination of atomic formulas, and the definition ensures that $\mathcal A$ and $\mathcal H$ agree on these.
If $k > 0$, then $G = \forall y G’$ for some $G’$ where $G’$ has one less quantifier than $G$. But then
\[\begin{aligned} \mathcal A \models G &\text{ iff } \mathcal A \models \forall y G' \\\\ &\text{ iff } \forall t \text{ ground term } \mathcal A, [y \mapsto t^\mathcal A] \models G' \\\\ &\text{ iff } \forall t \text{ ground term } \mathcal A \models G'[t/y] &&(1\star) \\\\ &\text{ iff } \forall t \text{ ground term } \mathcal H \models G'[t/y] && (2\star)\\\\ &\text{ iff } \forall t \text{ ground term } \mathcal H, [y \mapsto t] \models G' \\\\ &\text{ iff } \mathcal H \models G \end{aligned}\]where $(1\star)$ is justified by the translation lemma, and $(2\star)$ is justified by the inductive hypothesis.
Hence the induction is complete and the result is proven.
Herbrand expansions
Suppose:
- $\sigma$ is a signature
- $F = \forall x _ 1 \cdots \forall x _ n F^\ast$ is a closed formula in Skolem form
@Define the Herbrand expansion $E(F)$.
i.e. $E(F)$ is the (generally infinite) set obtained by substituting ground terms for the variables in $F^\ast$ in all possible ways.
@State a theorem which lets you reduce satisfiability of a first-order formula (without equality) to a propositional satisfiability problem.
Suppose:
- $F$ is a closed first-order formula
Then:
- $F$ is satisfiable iff $E(G)$ is satisfiable when considered as a set of propositional formulas
where $G$ is a corresponding equisatisfiable Skolem formula and $E(G)$ is the Herbrand expansion of $G$.
@Prove that if:
- $F$ is a closed Skolem formula
- $E(F)$ is the corresponding Herbrand expansion
Then:
- $F$ is satisfiable iff $E(F)$ is satisfiable when considered as a set of propositional formulas
Suppose
\[F = \forall x_1 \cdots \forall x_n F^\ast\]Then
\[\begin{aligned} F \text{ satisfiable} &\iff F \text{ has Herbrand model} \\\\ &\iff \exists \mathcal H \text{ s.t. } \mathcal H \models F \\\\ &\iff \exists \mathcal H \text{ s.t. } \forall t_i \text{ ground terms } \mathcal H, [x_1 \mapsto t_1], \ldots, [x_n \mapsto t_n] \models F \\\\ &\iff \exists \mathcal H \text{ s.t. } \forall t_i \text{ ground terms } \mathcal H \models F^\ast [t_1 / x_1]\cdots[t_n/x_n] \models F \\\\ &\iff \exists \mathcal H \text{ s.t. } \mathcal H \models E(F) \\\\ &\iff E(F) \text{ satisfiable} \end{aligned}\]where the initial implication is by Herbrand’s theorem.
Examples
Show that the first-order formula
\[F = \exists x_1 \exists x_2 \exists x_3 (\lnot(\lnot P(x_1) \to P(x_2)) \land \lnot (\lnot P(x_1) \to \lnot P(x_3)))\]
is satisfiable using Herbrand’s theorem.
Skolemizing, we obtain
\[G = (\lnot(\lnot P(a) \to P(b)) \land \lnot (\lnot P(a) \to \lnot P(c)))\]Then by Herbrand’s theorem, $G$ is satisfiable iff it has a Herbrand model. But then assigning $P(a) = 0$, $P(b) = 0$, $P(c) = 1$ satisfies $G$, so it is satisfiable.
@example~
Give two @examples of formulas that are satisfiable, but have no Herbrand model.
- Consider $F = \exists x R(x) \land \lnot R(c)$ over the signature with just one constant symbol and one predicate symbol. Clearly $F$ is satisfiable, but any Herbrand model with have just one element and so $F$ will not be satisfied.
- Consider $F = P(0) \land \forall x (P(x) \to P(s(x))) \land \exists x \lnot P(x)$ over the signature with one constant symbol $0$, one predicate $P(x)$, and one function $s$. Then any Herbrand model will have domain $\{0, s(0), s(s(0)), \ldots\}$. If it satisfies $F$, then inductively $P(0), P(s(0)), P(s(s(0))), \ldots$ must hold. Hence no $x$ satisfies $\lnot P(x)$. But $F$ is still satisfiable, e.g. with $\mathbb N \cup \{\infty\}$.
Give an @example of where Herbrand’s theorem fails in first-order logic with equality, i.e. find a first-order formula in Skolem form such that it is satisfiable but doesn’t have a Herbrand model.
Consider
\[F = \forall x [(f(x) \ne x) \land (f(f(x)) = x)]\]with constant $c$ and function symbol $f$. Then the domain of any Herbrand structure is $\{c, f(c), f(f(c), \ldots\}$. Hence $F$ is not satisfied.
But $F$ is satisfiable, e.g. by a model with domain $D = \{0, 1\}$ and $f^D(0) = 1$ and $f^D(1) = 0$.