Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav08:herbrand_universe_for_equality [2008/04/02 21:49] vkuncak |
sav08:herbrand_universe_for_equality [2008/04/02 21:49] 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 $S' \cup AxEq$ is satisfiable.** | + | 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$. Moreover, $I_Q(eq)$ is the identity relation, so $S$ is true under $I_Q$ as well. Therefore, **$S$ 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$. Moreover, $I_Q(eq)$ is the identity relation, so $S$ is true under $I_Q$ as well. Therefore, $S$ is satisfiable. |
| ===== Herbrand-Like Theorem for Equality ===== | ===== Herbrand-Like Theorem for Equality ===== | ||