Isomorphism of First-Order Logic Interpretations

(Building on First-Order Logic Semantics.)

Example: How many models does this formula have? 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  • for , and all  • 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:

reflexive:

symmetric:

transitive:

End of Proof Sketch.

Lemma: If is isomorphism from to , then for every first-order term we have 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.