Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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