Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
sav08:herbrand_universe_for_equality [2008/04/02 16:08] vkuncak |
sav08:herbrand_universe_for_equality [2008/04/02 20:40] vkuncak |
||
|---|---|---|---|
| Line 19: | Line 19: | ||
| For each element $t \in GT$, define | 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 | Let | ||
| Line 25: | Line 25: | ||
| [GT] = \{ [t] \mid t \in GT \} | [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) \} | 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. | + | 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 ===== | ===== Herbrand-Like Theorem for Equality ===== | ||