LARA

Herbrand Universe for Equality

Recall example of formula $F$:

\begin{equation*} P(a) \land (\forall x.\ P(x) \rightarrow \lnot P(f(x))) \land (\forall x. x=a \lor x=b) \end{equation*}

Replace '=' with 'eq':

\begin{equation*} P(a) \land (\forall x.\ P(x) \rightarrow \lnot P(f(x))) \land (\forall x. eq(x,a) \lor eq(x,b)) \end{equation*}

call the resulting formula $F'$.

Consider Herbrand model $I_H = (GT,\alpha_H)$ for the set $\{F'\} \cup AxEq$. The relation $\alpha_H(eq)$ splits $GT$ into two sets: the set of terms eq with $a$, and the set of terms eq with $b$. The idea is to consider these two partitions as domain of new interpretation, denoted $([GT], \alpha_Q)$.

Constructing Model for Formulas with Equality

Let $S$ be a set of formulas in first-order logic with equality and $S'$ result of replacing '=' with 'eq' in $S$. Suppose $S' \cup AxEq$ is satisfiable.

Let $I_H = (GT,\alpha_H)$ be Herbrand model for $S \cup AxEq$. We construct a new model as Interpretation Quotient Under Congruence of $(GT,\alpha)$ under congruence 'eq'. Denote quoient structure by $I_Q = ([GT],\alpha_Q)$. By theorem on quotient structures, $S$ is true in $I_Q$. Therefore, $S$ is satisfiable.

Herbrand-Like Theorem for Equality

Theorem: For every set of formulas with equality $S$ the following are equivalent

  1. $S$ has a model;
  2. $S' \cup AxEq$ has a model (where $AxEq$ are Axioms for Equality and $S'$ is result of replacing '=' with 'eq' in $S$);
  3. $S$ has a model whose domain is the quotient $[GT]$ of the set of ground terms under some congruence.