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(I_1)(t))=e_T(I_2)(t)
\]
and for every first-order logic formula we have
.
Proof:
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.