# Herbrand Universe for Equality

Recall example of formula :

Replace '=' with 'eq':

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 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 . Therefore, 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 the set of ground terms under some congruence.