LARA

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:

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) = $

$\alpha_2(f)(e_1,\ldots,e_n) = $

$((e_1,\ldots,e_n) \in \alpha_2(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.