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 21:43] vkuncak |
sav08:herbrand_universe_for_equality [2008/04/02 22:58] 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 $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$. 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. |