Completeness of the extension of first order logic with least fixed point order operator Is there any result about the extension of first order logic with least fixed point operator, being complete (as logic in general on infinite structures too) or not? In other words does the Goedel completeness theorem of first order logic extent to such FO-LFP logic ?
FO-LFP is neither complete (its valid sentences cannot be described by a recursively presented proof system) nor compact (there is an unsatisfiable set of sentences all of whose finite subsets are satisfiable). The basic argument is given in Denis’s answer so I won’t repeat it here, but let me instead point out that as a general principle due to Per Lindström, when extending first-order logic, some important property has to give way.

The setup is that we consider logics given by a satisfaction predicate $M\models\phi$ between ordinary first-order models, and an abstract set of sentences, that satisfy a handful of natural technical conditions.

The first Lindström’s theorem states that no proper extension of FO can simultaneously satisfy


(Löwenheim–Skolem) If a sentence has a model, it has an at most countable model.
(Compacteness) If $T$ is a set of sentences such that every finite subset of $T$ has a model, then $T$ has a model.


The second Lindström’s theorem states that no proper extension of FO with effectively presented syntax can satisfy


The Löwenheim–Skolem property as above.
(Completeness) The set of valid sentences can be described by an effectively axiomatized proof system (i.e., it is recursively enumerable).


For example, FO+TC has the Löwenheim–Skolem property (as it is a fragment of $L_{\omega_1,\omega}$), hence it can be neither complete nor compact, and a fortiori the same applies to all extensions of FO+TC such as fixed-point logics. (This is of course easy to show directly.)