This is an old revision of the document!
Herbrand Universe for Equality
Recall example of formula :
\[
P(a) \land (\forall x.\ P(x) \rightarrow \lnot P(f(x))) \land (\forall x. x=a \lor x=b)
\] Replace '=' with 'eq': \[
P(a) \land (\forall x.\ P(x) \rightarrow \lnot P(f(x))) \land (\forall x. eq(x,a) \lor eq(x,b))
\]
call the resulting formula .
Consider Herbrand model for the set
. The relation
splits
into two sets: the set of terms eq with
, and the set of terms eq with
.
Constructing Model for Formulas with Equality
Let be a set of formulas in first-order logic with equality and
result of replacing '=' with 'eq' in
. Suppose that
is satisfiable. Let
be Herbrand model for
. We construct a new model using quotient construction, described as follows.
For each element , define
\[
[t] = \{ s \mid (s,t) \in I_H(eq) \}
\] Let \[
[GT] = \{ [t] \mid t \in GT \}
\]
The constructed model will be where
\[
I_Q(f) = \{ ([t_1],\ldots,[t_n], [f(t_1,\ldots,t_n)]) \mid t_1,\ldots,t_n \in GT \}
\] \[
I_Q(R) = \{ ([t_1],\ldots,[t_n]) \mid (t_1,\ldots,t_n) \in I_H(R) \}
\]
Consequently, \[
I_Q(eq) = \{ ([t_1],[t_2]) \mid (t_1,t_2) \in I_H(eq) \} = \{ (a,a) \mid a \in [GT] \}
\]
that is, the interpretation of eq in is equality.
Herbrand-Like Theorem for Equality
Theorem: For every set of formulas with equality the following are equivalent
has a model
has a model whose domain is the quotient
of ground terms under some congruence