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]
Line 1: Line 1:
-====== Isomorphism of First-Order Logic Interpretations ====== 
- 
-(Building on [[First-Order Logic Semantics]].) 
- 
-**Example:​** How many models does this formula have? 
-\[\begin{array}{l} 
-    (\exists x. P(x))\ \land \\  
-    (\exists x. \lnot P(x))\ \land \\  
-    (\forall x. \forall y. P(x) \land P(y) \rightarrow x=y)\ \land \\ 
-    (\forall x. \forall y. \lnot P(x) \land \lnot P(y) \rightarrow x=y) \\ 
-\end{array} 
-\] 
-++Answer:​|Infinitely many.  For example, for any integer $n$, let $I=(D,​\alpha)$ such that $D=\{n,​n+1\}$ and $\alpha(P)=\{n\}$.++ 
- 
-Informally, isomorphism is a function that establishes correspondence between two interpretations. 
- 
-**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$ 
-\[ 
-   ​((x_1,​\ldots,​x_n) \in \alpha_1(R)) \leftrightarrow (s(x_1),​\ldots,​s(x_n)) \in \alpha_2(R)) 
-\] 
-  * for $f \in {\cal L}$, $ar(f)=n$ and all $x_1,​\ldots,​x_n \in D_1$ 
-\[ 
-    s(\alpha_1(f)(x_1,​\ldots,​x_n)) = \alpha_2(f)(s(x_1),​\ldots,​s(x_n)) 
-\] 
-  * 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//​. 
- 
-**Definition:​** Interpretation $I_1$ is //​isomorphic//​ to interpretation $I_2$ if there exists an isomorphism from $I_1$ to $I_2$. 
- 
-Note: the notion of graph isomorphisms is a special case of isomorphism of structures because we can view [[Graphs as Interpretations]]. 
- 
-**Lemma:** Being isomorphic is reflexive, symmetric, and transitive property. 
-**Proof sketch:** 
- 
-++++reflexive:​| take the identiy function $s(d)=d$ as the isomorphism++++ 
- 
-++++symmetric:​| if $I_1$ is isomorphic to $I_2$ with $s$, then $I_2$ is isomorphic to $I_1$ with $s^{-1}$++++ 
- 
-++++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}  ​ 
-    (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(\alpha_2(f)(s_1(x_1),​\ldots,​s_1(x_n))) \\ 
-&=& \alpha_3(f)(s_2(s_1(x_1),​\ldots,​s_2(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 of Proof Sketch.** 
- 
-**Lemma:** If $s$ is isomorphism from $I_1$ to $I_2$, then for every first-order term $t$ we have 
-\[ 
-   ​s(e_T(t)(I_1))=e_T(t)(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. 
- 
-Case for $F_1 \land F_2$. 
- 
-Case for $\exists x.F$.  Induction issues. 
- 
-++ 
- 
-**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)$. 
- 
-**Proof:** We construct $\alpha_2$ from $\alpha_1$ and $s$. 
- 
-$\alpha_2(x) = $++|$s(\alpha_1(x))$ ++ 
- 
-$\alpha_2(f)(e_1,​\ldots,​e_n) = $++|$s(\alpha_1(f)(s^{-1}(e_1),​\ldots,​s^{-1}(e_n))$ ++ 
- 
-$((e_1,​\ldots,​e_n) \in \alpha_2(R)) = $++|$((s^{-1}(e_1),​\ldots,​s^{-1}(e_n)) \in \alpha_1(R))$ ++ 
- 
-**End of proof.** 
- 
-**Corollary:​** Consider an interpretation $(D_1,​\alpha_1)$. ​ If $D_1$ is finite, then there exists isomorphic interpretation $(D_2,​\alpha_2)$ where $D_2 = \{1,​\ldots,​n\}$. 
- 
-Also, note that for each permutation of $\{1,​\ldots,​n\}$ there is an automorphism that generates potentially a new interpretation. ​ There are $n!$ permutations. 
- 
-These observations are relevant for [[Finite-Model Finders]].