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 20:36] vkuncak |
sav08:herbrand_universe_for_equality [2008/04/02 20:45] vkuncak |
||
|---|---|---|---|
| Line 15: | Line 15: | ||
| ===== Constructing Model for Formulas with Equality ===== | ===== 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 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 (recall notation in [[First-Order Logic Semantics]]). |
| For each element $t \in GT$, define | For each element $t \in GT$, define | ||
| Line 33: | Line 33: | ||
| \] | \] | ||
| - | Consequently, | + | 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] \} | + | $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. | that is, the interpretation of eq in $([GT],I_Q)$ is equality. | ||
| + | ++ | ||