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:40] vkuncak |
sav08:herbrand_universe_for_equality [2008/04/02 21:49] vkuncak |
||
---|---|---|---|
Line 11: | Line 11: | ||
call the resulting formula $F'$. | call the resulting formula $F'$. | ||
- | 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$. | + | 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 ===== | ===== 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 | + | |
- | \[ | + | |
- | [t] = \{ s \mid (s,t) \in I_H(eq) \} | + | |
- | \] | + | |
- | Let | + | |
- | \[ | + | |
- | [GT] = \{ [t] \mid t \in GT \} | + | |
- | \] | + | |
- | The constructed model will be $([GT],I_Q)$ where | + | |
- | \[ | + | |
- | 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) \} | + | |
- | \] | + | |
- | + | ||
- | 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. | + | |
- | ++ | + | |
+ | 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 ===== | ||
**Theorem:** For every set of formulas with equality $S$ the following are equivalent | **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 ground terms under some congruence |