Stability theory, permutations of indiscernibles, and embedded finite models

We show that the expressive power of first-order logic over finite models embedded in a model $M$ is determined by stability-theoretic properties of $M$. In particular, we show that if $M$ is stable, then every class of finite structures that can be defined by embedding the structures in $M$, can be defined in pure first-order logic. We also show that if $M$ does not have the independence property, then any class of finite structures that can be defined by embedding the structures in $M$, can be defined in first-order logic over a dense linear order. This extends known results on the definability of classes of finite structures and ordered finite structures in the setting of embedded finite models. These results depend on several results in infinite model theory. Let $I$ be a set of indiscernibles in a model $M$and suppose $(M,I)$ is elementarily equivalent to $(M_1,I_1)$ where $M_1$ is $\vert I_1\vert^+$-saturated. If $M$ is stable and $(M,I)$ is saturated, then every permutation of $I$extends to an automorphism of $M$ and the theory of $(M,I)$ is stable. Let $I$ be a sequence of $<$-indiscernibles in a model $M$, which does not have the independence property, and suppose $(M,I)$ is elementarily equivalent to $(M_1,I_1)$ where $(I_1,<)$ is a complete dense linear order and $M_1$ is $\vert I_1\vert^+$-saturated. Then $(M,I)$-types over $I$are order-definable and if $(M,I)$ is $\aleph_1$-saturated, every order preserving permutation of $I$ can be extended to a back-and-forth system.