# 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 ?

• The same question can be asked for the existential part only of first order logic, when extended by fixed point order operator, which still captures Ptime complexity. – Constantine Kyritsis Jun 16 '14 at 6:49
• @Kaveh: You are mixing up two unrelated meanings of the word “complete”. Ordinary first-order logic is not complete in your sense either, and this has nothing to do with the completeness theorem. – Emil Jeřábek Jun 19 '14 at 10:48
• @Emil, you are right. – Kaveh Jun 19 '14 at 14:35

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

1. (Löwenheim–Skolem) If a sentence has a model, it has an at most countable model.

2. (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

1. The Löwenheim–Skolem property as above.

2. (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.)

It does not extend.

Consider FO-LFP with just a binary predicate $<$, and the axioms for $<$ being a total order, with first and last positions, and every position has a successor. Moreover, we add an axiom saying that the last position can be reached from the first by iterating the successor function as a smallest fixpoint. This ensures that the universe is finite.

Now for each $n$, we can build a formula $\varphi_n$ stating that the universe has at least $n$ positions. Let $\Gamma=\{\varphi_n:n\in\mathbb N\}$

Each finite subset of $\Gamma$ has a model, but $\Gamma$ does not, so the compactness theorem fails.

• Your construction starts in the right direction, but the failure of compactness is irrelevant. What you need to actually answer the question is to take the axiom, and use it to show that the set of true arithmetic sentences is recursively reducible to FO-LFP validity, which implies the latter is not complete with respect to any recursively axiomatized proof system. – Emil Jeřábek Jun 19 '14 at 10:45
• oups you're right I went too fast, mistook completeness for compactness, thanks – Denis Jun 19 '14 at 13:34

I found a paper here that somehow gives a kind of completeness of the existential part of FO-LFP. This still captures polynomial time complexity in the sense of complete recursive enumerable set of valid statements existential FO-LFP, which of course is not the Gödel completeness of FO.