Lab for Automated Reasoning and Analysis 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:isomorphism_of_interpretations [2008/03/19 17:34]
vkuncak
sav08:isomorphism_of_interpretations [2015/04/21 17:30] (current)
Line 4: Line 4:
  
 **Example:​** How many models does this formula have? **Example:​** How many models does this formula have?
-\[\begin{array}{l}+\begin{equation*}\begin{array}{l}
     (\exists x. P(x))\ \land \\      (\exists x. P(x))\ \land \\ 
     (\exists x. \lnot P(x))\ \land \\      (\exists x. \lnot P(x))\ \land \\ 
Line 10: Line 10:
     (\forall x. \forall y. \lnot P(x) \land \lnot P(y) \rightarrow x=y) \\     (\forall x. \forall y. \lnot P(x) \land \lnot P(y) \rightarrow x=y) \\
 \end{array} \end{array}
-\]+\end{equation*}
 ++Answer:​|Infinitely many.  For example, for any integer $n$, let $I=(D,​\alpha)$ such that $D=\{n,​n+1\}$ and $\alpha(P)=\{n\}$.++ ++Answer:​|Infinitely many.  For example, for any integer $n$, let $I=(D,​\alpha)$ such that $D=\{n,​n+1\}$ and $\alpha(P)=\{n\}$.++
  
Line 17: Line 17:
 **Definition:​**:​ An isomoprhism between $(D_1,​\alpha_1)$ and $(D_2,​\alpha_2)$ is a //bijective function// $s : D_1 \to D_2$ such that **Definition:​**:​ An isomoprhism between $(D_1,​\alpha_1)$ and $(D_2,​\alpha_2)$ is a //bijective function// $s : D_1 \to D_2$ such that
   * for $R \in {\cal L}$, $ar(R)=n$ and all $x_1,​\ldots,​x_n \in D_1$   * for $R \in {\cal L}$, $ar(R)=n$ and all $x_1,​\ldots,​x_n \in D_1$
-\[+\begin{equation*}
    ​((x_1,​\ldots,​x_n) \in \alpha_1(R)) \leftrightarrow (s(x_1),​\ldots,​s(x_n)) \in \alpha_2(R))    ​((x_1,​\ldots,​x_n) \in \alpha_1(R)) \leftrightarrow (s(x_1),​\ldots,​s(x_n)) \in \alpha_2(R))
-\]+\end{equation*}
   * for $f \in {\cal L}$, $ar(f)=n$ and all $x_1,​\ldots,​x_n \in D_1$   * for $f \in {\cal L}$, $ar(f)=n$ and all $x_1,​\ldots,​x_n \in D_1$
-\[+\begin{equation*}
     s(\alpha_1(f)(x_1,​\ldots,​x_n)) = \alpha_2(f)(s(x_1),​\ldots,​s(x_n))     s(\alpha_1(f)(x_1,​\ldots,​x_n)) = \alpha_2(f)(s(x_1),​\ldots,​s(x_n))
-\]+\end{equation*}
   * for $x \in V$ a first-order variable, $s(\alpha_1(x)) = \alpha_2(x)$.   * for $x \in V$ a first-order variable, $s(\alpha_1(x)) = \alpha_2(x)$.
 If $D_1=D_2$ then the isomorphism $s$ is called //​automorphism//​. If $D_1=D_2$ then the isomorphism $s$ is called //​automorphism//​.
Line 39: Line 39:
  
 ++++transitive:​| if $s_1 : I_1 \to I_2$ is isomorphism and $s_2 : I_2 \to I_3$ is isomorphism,​ then we claim $s_2 \circ s_1 : I_1 \to I_3$ is isomorphism. ​ Let us prove this for the case of function symbols: ++++transitive:​| if $s_1 : I_1 \to I_2$ is isomorphism and $s_2 : I_2 \to I_3$ is isomorphism,​ then we claim $s_2 \circ s_1 : I_1 \to I_3$ is isomorphism. ​ Let us prove this for the case of function symbols:
-\[\begin{array}{rcl}  ​+\begin{equation*}\begin{array}{rcl}  ​
     (s_2 \circ s_1)(\alpha_1(f)(x_1,​\ldots,​x_n)) ​     (s_2 \circ s_1)(\alpha_1(f)(x_1,​\ldots,​x_n)) ​
 &=& s_2(s_1(\alpha_1(f)(x_1,​\ldots,​x_n))) \\ &=& s_2(s_1(\alpha_1(f)(x_1,​\ldots,​x_n))) \\
Line 46: Line 46:
 &=& \alpha_3(f)((s_2 \circ s_1)(x_1),​\ldots,​(s_2 \circ s_1)(x_n))) ​ &=& \alpha_3(f)((s_2 \circ s_1)(x_1),​\ldots,​(s_2 \circ s_1)(x_n))) ​
 \end{array} \end{array}
-\]+\end{equation*}
 ++++ ++++
  
Line 52: Line 52:
  
 **Lemma:** If $s$ is isomorphism from $I_1$ to $I_2$, then for every first-order term $t$ we have **Lemma:** If $s$ is isomorphism from $I_1$ to $I_2$, then for every first-order term $t$ we have
-\[+\begin{equation*}
    ​s(e_T(t)(I_1))=e_T(t)(I_2)    ​s(e_T(t)(I_1))=e_T(t)(I_2)
-\]+\end{equation*}
 and for every first-order logic formula $F$ we have $e_F(F)(I_1)=e_F(F)(I_2)$. and for every first-order logic formula $F$ we have $e_F(F)(I_1)=e_F(F)(I_2)$.
  
-**Proof:** ++|Induction on the structure of terms and formulas.+**Proof:​** ​++++|Induction on the structure of terms and formulas.
  
 Case for $F_1 \land F_2$. Case for $F_1 \land F_2$.
  
-Case for $\exists x.F$.  Induction issues.+Case for $\exists x.F$.  Induction issues, function update on isomorphic interpretations.
  
-+++++++
  
 **Lemma:** If $(D_1,​\alpha_1)$ is an interpretation for language ${\cal L}$, if $D_2$ is a set and $s : D_1 \to D_2$ a bijective function, then there exists a mapping $\alpha_2$ of symbols in ${\cal L}$ such that $(D_2,​\alpha_2)$ is an interpretation for ${\cal L}$ and $(D_2,​\alpha_2)$ is isomorphic to $(D_1,​I_1)$. **Lemma:** If $(D_1,​\alpha_1)$ is an interpretation for language ${\cal L}$, if $D_2$ is a set and $s : D_1 \to D_2$ a bijective function, then there exists a mapping $\alpha_2$ of symbols in ${\cal L}$ such that $(D_2,​\alpha_2)$ is an interpretation for ${\cal L}$ and $(D_2,​\alpha_2)$ is isomorphic to $(D_1,​I_1)$.
 
sav08/isomorphism_of_interpretations.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice