Power of First Order Logic with Least Fixed Points

Consider first order logic augmented by least fixed point operator in the following way: For any formula F in which a predicate P appears only positively, the following are added to FOL.
  - a new predicate symbol F* (intended to be the fixed point of F)
-  axiom stating that F* is a fixed point for F
-  axiom stating that F* is contained in every fixed point of F.
It is easy to see that F* might not be the least fixed point of F since it is least only with respect to fixed points definable in this system, and that this system does not have a sound and complete proof system.

The work presented here examines if this system can prove "natural" statements involving fixed points. As a motivating example of a natural statement, we considered the following:  Let A by a monotone operator on binary relations such that if the graph of a predicate P is a partial function, so is A(P), and provably so. Then, A* is a partial function. 

We showed that this is provable within the system, and defined a subclass of statements provable by the system. Future works include trying to determine the power of this system.