Unexpressibility of a property in first order logic We can give a very general notion of what is to iterate a function. Given a set $\mathcal U$ and a function $f:\mathcal U \rightarrow \mathcal U$, then, to iterate the function $f$ will mean to compose f with itself. We can also define $f_0=f$ and $f_n = f \circ f_{n-1}$for any $n \in \mathbb N$. With this notation, an iteration of $f$ will be any of the functions $f_n$.
Now comes the question. We are given a nonempty set $\mathcal U$, an elemtent $\alpha \in \mathcal U$ and a function $f:\mathcal U \rightarrow \mathcal U$. Can we express in first order logic the property that for any $x \in \mathcal U$ there exists an $n \in \mathbb N_0$ with $f_n(x)=\alpha$?
More precisely: given a first order language $\mathcal L = \langle\mathcal U, =, c,f\rangle$ where $c$ is a constant symbol and $f$ is a unary function symbol, is the class of models with the aforementioned property definable in first order? That is, does there exists a first order sentence $\phi$ such that its satisfied only by the models of $\mathcal L$ with the property?
I've been thinking about this for a while but nothing came out. I guess that the property is not definable in first order and that this can be proved using the compactness theorem, but I don't know how.
If the property turns out to be undefinable it may be useful to construct models with unbounded $n$ to get a proof. For example, I took $\mathcal U = \mathbb N$, $c = 1$ and $f$ defined by $f(1)=1$ and $f(x)=x-1$ for any $x$ grater than $1$.
Thanks
 A: No, the class of models with the property that $(\forall x)(\exists n)[c = f^n(x)]$ is not an elementary class in the language $\{f, c, =\}$. This is a relatively typical exercise using the compactness theorem.  The main idea in the proof is that, for a fixed $x$, the least $n$ that works can be arbitrarily large.  In particular, $\{ f^n(c') \not = c : n \in \omega\}$ is finitely consistent in the language $\{f, c, c', =\}$.  Take a model of that set of sentences, and then reduce the language back to the original, smaller one. 
A: Here's another way of seeing why this admits a negative answer.
For every $n>1$ pick some finite structure with $n$ elements, such that $f$ is a cyclic permutation. Of course this would satisfy this property, but we require more and more iterations of $f$ in order to ensure that $c$ is reached.
Now take the ultraproduct of these structure, over any free ultrafilter over $\Bbb N$.
Since each structure satisfied the property "$f$ is a permutation of the universe", the result is an injective function $f$. But this means that there is only a countable set of elements which are in the orbit of $c$ which has any chance of reaching $c$ at some iteration of $f$. On the other hand, simple cardinality arguments show that the model we get by the ultraproduct is uncountable, so at least one (and in fact most) elements cannot reach $c$ by iterating $f$.
