This is an old revision of the document!
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:
Informally, isomorphism is a function that establishes correspondence between two interpretations.
Definition:: An isomoprhism between and is a bijective function such that
- for , and all
\[
((x_1,\ldots,x_n) \in \alpha_1(R)) \leftrightarrow (s(x_1),\ldots,s(x_n)) \in \alpha_2(R))
\]
- for , and all
\[
s(\alpha_1(f)(x_1,\ldots,x_n)) = \alpha_2(f)(s(x_1),\ldots,s(x_n))
\]
- for a first-order variable, .
If then the isomorphism is called automorphism.
Definition: Interpretation is isomorphic to interpretation if there exists an isomorphism from to .
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:
End of Proof Sketch.
Lemma: If is isomorphism from to , then for every first-order term we have \[
s(e_T(t)(I_1))=e_T(t)(I_2)
\] and for every first-order logic formula we have .
Lemma: If is an interpretation for language , if is a set and a bijective function, then there exists a mapping of symbols in such that is an interpretation for and is isomorphic to .
Proof: We construct from and .
End of proof.
Corollary: Consider an interpretation . If is finite, then there exists isomorphic interpretation where .
Also, note that for each permutation of there is an automorphism that generates potentially a new interpretation. There are permutations.
These observations are relevant for Finite-Model Finders.