Existence of a prime model for a theory Consider the language $\mathcal{L} = \{P, f\}$ with $P$ a unary predicate and $f$ a unary function. Let $T$ be the theory:


*

*$f$ is a bijection

*$\forall x \, f^nx \neq x$ for all $n$

*$\forall x \, (Px \to Pfx)$

*there are infinitely many elements not satisfying $P$ whose $f$-image does satisfy $P$.


Two question about this theory:


*

*Show that $T$ has a prime model.

*Determine all complete 1-types and indicate which of these are isolated.


I am stuck on this exercise. In general I don't know how to approach an exercise like this.
With regard to the existence of a prime model, I can only think to show that $T$ is complete and its isolated types are dense. This in turn "reduces" to showing that $T$ has at most countably many types.
 A: Your solution via QE outlined in the comments is essentially correct, except for the hitch that $T$ doesn't quite have QE in the given language: for example, the formula $\exists y\, (P(y)\land f(y) = x)$ isn't equivalent to a quantifier-free formula. The problem here is that $f^{-1}$ isn't in the language. This leads to a hole in your argument, since if $m$ is an element such that $M\models P(m)$ but $M\not\models P(f^{-1}(m))$, we could map $m$ by a local isomorphism to any element $n$ such that $N\models P(n)$, including one where $N\models P(f^{-1}(n))$ and $N\not\models P(f^{-2}(n))$ (since $f^{-1}(m)$ is not in the substructure of $M$ generated by $m$).  
But we can fix this by a definitional expansion. Let $\mathcal{L}' = \{P,f,g\}$, and let $$T' = T\cup \{\forall x \forall y\, (g(x) = y  \leftrightarrow f(y) = x)\}.$$
We say that $T'$ is a definitional expansion of $T$, because it is obtained by adding new symbols to the language (in this case just $g$) and new axioms explicitly defining these new symbols in terms of formulas in the original language. 
In case you are not familiar with the concept of definitional expansion: It follows that every model $M$ of $T$ expands in a unique way to a model $M'$ of $T'$, every $\mathcal{L'}$-formula $\varphi'(x)$ has a corresponding $\mathcal{L}$-formula $\varphi(x)$ (obtained by replacing instances of the new symbols by their definitions in terms of the old symbols) such that $M'\models \varphi'(a)$ if and only if $M\models \varphi(a)$, and $f\colon M\to N$ is an $\mathcal{L}$-elementary embedding if and only if $f\colon M'\to N'$ is an $\mathcal{L}'$-elementary embedding. So the definitional expansion does not change the answers to your questions: $M$ is a prime model of $T$ if and only if $M'$ is a prime model of $T'$, restriction to formulas in $\mathcal{L}$ is a bijection from types relative to $T'$ to types relative to $T$, and a type relative to $T'$ is isolated (by $\varphi'(x)$) if and only if its restriction to $\mathcal{L}$ is isolated (by $\varphi(x)$).
Now you can prove that $T'$ has QE (as you outlined in the comments), use this to answer your questions, and then conclude by taking the reduct to $\mathcal{L}$. 
