Differences

This shows you the differences between two versions of the page.

--- sav08:herbrand_universe_for_equality [2008/04/02 15:51]
vkuncak
+++ sav08:herbrand_universe_for_equality [2008/04/02 22:59]
vkuncak
@@ Line 11: / Line 11: @@
 call the resulting formula $F'$.
-Consider Herbrand model $I_H$ for $\{F'\} \cup AxEq$.  The relation $e_F(I_H)(eq)$ splits $GT$ into two sets: the set of terms eq with $a$, and the set of terms eq with $b$.
+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 that $S \cup AxEq$ is satisfiable.  Let $(GT,I_H)$ be Herbrand model for $S \cup AxEq$.  We construct a new model using //quotient// construction, described as follows.
+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.
-For each element $t \in GT$, define
+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.
-\[
-    [t] = \{ s \mid (s,t) \in e_F(I_H)(eq) \}
-\]
-Let
-\[
-    [GT] = \{ [t] \mid t \in GT \}
-\]
-The constructed model will be $([GT],I_Q)$ where $I_Q$ is such that
-\[
-    I_Q(f)([t_1],\ldots,[t_n]) = [f(t_1,\ldots,t_n)]
-\]
-\[
-    I_Q(R) = \{ ([t_1],\ldots,[t_n]) \mid (t_1,\ldots,t_n) \in I_H(R) \}
-\]
-The interpretation of eq in $([GT],I_Q)$ becomes equality.
-Inductive lemma.
 ===== Herbrand-Like Theorem for Equality =====
 **Theorem:** For every set of formulas with equality $S$ the following are equivalent
-  * $S$ has a model
+  - $S$ has a model;
-  * $S' \cup AxEq$ has a model (where $AxEq$ are [[Axioms for Equality]] and $S'$ is result of replacing '=' with 'eq' in $S$)
+  - $S' \cup AxEq$ has a model (where $AxEq$ are [[Axioms for Equality]] and $S'$ is result of replacing '=' with 'eq' in $S$);
-  * $S$ has a model whose domain is the quotient $[GT]$ of ground terms under some congruence
+  - $S$ has a model whose domain is the quotient $[GT]$ of the set of ground terms under some congruence.