Differences

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

--- sav08:herbrand_universe_for_equality [2008/04/02 14:08]
vkuncak
+++ sav08:herbrand_universe_for_equality [2008/04/02 20:40]
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 $(GT,I_H)$ for the set $\{F'\} \cup AxEq$.  The relation $I_H(eq)$ splits $GT$ into two sets: the set of terms eq with $a$, and the set of terms eq with $b$.
 ===== Constructing Model for Formulas with Equality =====
@@ Line 19: / Line 19: @@
 For each element $t \in GT$, define
 \[
-    [t] = \{ s \mid (s,t) \in e_F(I_H)(eq) \}
+    [t] = \{ s \mid (s,t) \in I_H(eq) \}
 \]
 Let
@@ Line 25: / Line 25: @@
     [GT] = \{ [t] \mid t \in GT \}
 \]
-The constructed model will be $([GT],I_Q)$ where $I_Q$ is such that
+The constructed model will be $([GT],I_Q)$ where
 \[
-    I_Q(f)([t_1],\ldots,[t_n]) = [f(t_1,\ldots,t_n)]
+    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) \}
 \]
-The interpretation of eq in $([GT],I_Q)$ becomes equality.
+In particular, when $R$ is $eq$ we have
+$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 $([GT],I_Q)$ is equality.
+++
 ===== Herbrand-Like Theorem for Equality =====