Isomorphism of First-Order Logic Interpretations

(Building on First-Order Logic Semantics.)

Example: How many models does this formula have?

$\begin{equation*}\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} \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\}$ .

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$

$\begin{equation*} ((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$

$\begin{equation*} 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)$ .

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:

symmetric:

transitive:

End of Proof Sketch.

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) \end{equation*}$

and for every first-order logic formula $F$ we have $e_F(F)(I_1)=e_F(F)(I_2)$ .

Proof:

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.