<p>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.</p>

<p>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.</p>

<p>The <em>first Lindström’s theorem</em> states that no proper extension of FO can simultaneously satisfy</p>

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

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

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

<p>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.)</p>

CC BY-SA 3.0
2014-06-19T12:20:28.000Z
2014-06-19T12:20:28.000Z
Emil Jeřábek
<p>It does not extend.</p>

<p>Consider FO-LFP with just a binary predicate $&lt;$, and the axioms for $&lt;$ 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.</p>

<p>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\}$</p>

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

CC BY-SA 3.0
2014-06-19T10:45:52.517Z
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
CC BY-SA 3.0
2014-06-19T13:34:27.987Z
oups you're right I went too fast, mistook completeness for compactness, thanks
Denis
CC BY-SA 3.0
2014-06-17T15:31:48.417Z
2014-06-20T22:57:15.073Z
2014-06-20T22:57:15.073Z
Denis
<p>I found a paper <a href="http://research.microsoft.com/en-us/um/people/gurevich/opera/73.pdf" rel="nofollow">here</a> 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&ouml;del completeness of FO.</p>

CC BY-SA 3.0
2014-06-20T06:47:12.930Z
2014-06-21T09:22:47.283Z
2014-06-21T09:22:47.283Z
Constantine Kyritsis
<p>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 ?</p>

CC BY-SA 3.0
2014-06-16T06:49:59.753Z
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
CC BY-SA 3.0
2014-06-19T10:48:38.873Z
@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
CC BY-SA 3.0
2014-06-19T14:35:50.590Z
@Emil, you are right.
Kaveh
<descriptive-complexity><logic-programming>
Completeness of the extension of first order logic with least fixed point order operator
Constantine Kyritsis
# Completeness of the extension of first order logic with least fixed point order operator

(Asked by: username_0 on 2014-06-16)

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 ?

**Tags:** descriptive-complexity, logic-programming
> **Comments:**
> **username_0**: 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.  
> **username_1**: @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.  
> **username_2**: @Emil, you are right.  

---

## 3 answers

### Answer by username_1 on 2014-06-19. Score: 8

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


---

### Answer by username_3 on 2014-06-17. Score: 2

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.

> **Comments:**
> **username_1**: 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.  
> **username_3**: oups you're right I went too fast, mistook completeness for compactness, thanks  

---

### Answer by username_0 on 2014-06-20. Score: -1

I found a paper [here](http://research.microsoft.com/en-us/um/people/gurevich/opera/73.pdf) 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.


---

