# 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:**

**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.