Differences
This shows you the differences between two versions of the page.
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]]. | ||