LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
sav08:herbrand_universe_for_equality [2008/04/02 21:49]
vkuncak
sav08:herbrand_universe_for_equality [2008/04/02 22:59]
vkuncak
Line 17: Line 17:
 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$. ​ 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 the set of ground terms under some congruence