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 . The idea is to consider these two partitions as domain of new interpretation, denoted .
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 $S' \cup AxEq$ is satisfiable.
Let be Herbrand model for . We construct a new model as Interpretation Quotient Under Congruence of under congruence 'eq'. Denote quoient structure by . By theorem on quotient structures, is true in . Moreover, is the identity relation, so is true under as well. Therefore, $S$ is satisfiable.
Herbrand-Like Theorem for Equality
Theorem: For every set of formulas with equality the following are equivalent
- has a model
- has a model (where are Axioms for Equality and is result of replacing '=' with 'eq' in )
- has a model whose domain is the quotient of ground terms under some congruence