Finding a model that realizes a non-principal type infinitely many times The following is a problem from an old qualifying exam:

Let $T$ be a complete consistent theory in a countable language, and let $\Sigma$ be a non-principal type of $T$. Prove that $T$ has a countable model $\mathcal{A}$ in which $\Sigma$ is realized infinitely many times.

(Here, a non-principal type is a non-isolated type, so for any formula $\varphi(\bar{x})$ consistent with $T$, there exists $\sigma(\bar{x}) \in \Sigma$ such that $\varphi \land \lnot \sigma$ is consistent with $T$.)
To try and prove this statement, I first read the response to this similar question; using the outline given in the response, I showed that there must be some model of $T$ that realizes $\Sigma$ at least two times. My hope was then to show that there are models of $T$ that realize $\Sigma$ an arbitrarily large finite number of times and apply the compactness theorem to conclude. However, I could not make the argument generalize past the "two realizations" case.
Is there a way to make this generalization work? Is there a better approach to this problem in the first place?
 A: Well, the natural compactness argument would be:

Add infinitely many new constant symbols $c_i$ (for $i\in\mathbb{N}$) to our language, and consider the theory $$T\cup\{c_i\not=c_j: i\not=j\}\cup\{\varphi(c_i): \varphi\in\Sigma,i\in\mathbb{N}\}.$$ By showing that this new theory is finitely satisfiable, we get a model of it.

Of course the difficulty is showing finite satisfiability. However, there's one immediate simplification we can make: it's enough to show that for each $\varphi\in\Sigma$ the set $T\cup\{c_i\not=c_j: i\not=j\}\cup\{\varphi(c_i): i\in\mathbb{N}\}$ is finitely satisfiable (do you see why?).
Now we come to the key result:

*

*For every formula $\theta$, if there are only finitely many types containing $\theta$ then every type containing $\theta$ is isolated.

If you can prove that you'll be done: since $\varphi\in\Sigma$ and $\Sigma$ is non-isolated we can pick infinitely many distinct types extending $\varphi$ and just give each one a $c_i$. This automatically handles the "$c_i\not=c_j$"-requirements since the different $c_i$s will have different types. (Note that there's a bit of irony here: we ultimately want to build a bunch of elements with the same type, so in our compactness argument we're going to deliberately grab elements with different types to make our lives easier.)
