this is a very old post so you might have already encountered the answer as desired. Since I have been studying FO(LFP) for the past few months. I have some understanding of the answers you require.
To answer the requirement of positivity, the need comes from the fact that testing whether the formula captures a monotone operator or not is undecidable both in finite and infinite models. What do I mean by a formula capturing a monotone operator?
Suppose you write out a FO$[\sigma$] formula with a free second order variable say $\phi(\vec{x},X)$, where $|\vec{x}|=ar(X)$, then we can define a corresponding operator $f_\phi$ : $\mathcal{P}(A^{ar(X)}) \mapsto \mathcal{P}(A^{ar(x)})$ where ar(X) is the arity of the second order variable and A is the domain of the $\sigma$-structure $\mathbb{A}$ and $\mathcal{P}(Z)$ is the power set of the set Z. And $f_\phi(Z) = \{\ \vec{a} \in A^{ar(X)}\ |\ \mathbb{A},\vec{a},Z \models \phi\ \} $. If this operator is monotone then we can easily capture the fixed point in both finite and infinite structure following the knaster tarski's fixed point theorem mentioned in the above answers. But, the problem is testing whether the formula written out of the form as above encodes a monotone operator or not is undecidable so we need to get the next best thing. Positivity in the second order free variable ensures the monotonicity requirement is met, its a standard structural induction to prove this phenomenon. Question is, is it enough?
To that, I have no solid answer yet, since I'm still reading. I can point to papers on this front. At least the one explaining ideas I mentioned here, are from the paper, Monotone vs Positive - Ajtai, Gurevich. It also further mentions another paper Fixed point extensions of first order logic by Gurevich and Shelah that states the fixed point operator when applied to the positive formula doesn't lose expressive power when compared with the application being done over arbitrary monotone formulas.