<p>There is a famous example of <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.56.3003">Cai, Fürer and Immerman</a>, which shows that the $\mathcal{C}_{\infty\omega}^k$-hierarchy is strict and in particular that $\mathcal{C}_{\infty\omega}^\omega$ cannot express every query on finite structures. The paper is quite famous because it disproved a conjecture that IFP+C captures PTIME. Your proof that $\mathcal{L}_{\infty\omega}\equiv\mathcal{C}_{\infty\omega}$ is correct. </p>

CC BY-SA 3.0
2014-07-05T22:26:01.920Z
2014-07-05T22:26:01.920Z
Sebastian Siebertz
<p>I'm trying to put together a general picture of the expressiveness of some logics: First-Order Logics, Fixed-Point Logics, (Finite Variable) Infinitary Logics and the respected versions with Counting. (<a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.33.726" rel="nofollow noreferrer">Source</a>)</p>

<p>$\mathcal{L}^k_{\infty\omega}$ is infinitary logic with $k$ distinct variables and </p>

<p>$$\mathcal{L}^\omega_{\infty\omega} := \bigcup_{k \in \omega}  \mathcal{L}^k_{\infty\omega}$$</p>

<p>is finite variable infinitary logic. (Analog for Counting)</p>

<p>This is in the context of Finite Model Theory so in general all structures are finite.</p>

<blockquote>
  <p>We say  $\varphi$ and $\varphi'$ are equivalent if for every structure
  $\mathcal A$</p>
  
  <p>$$ \mathcal A \models_\mathcal L \varphi \Leftrightarrow \mathcal A
&gt; \models_{\mathcal {L'}}  \varphi'.$$</p>
  
  <p>If for every $\mathcal L$-sentence there is a equivalent
  $\mathcal L'$-sentence we write</p>
  
  <p>$$ \mathcal L \leqq \mathcal L'.$$</p>
</blockquote>

<p><img src="https://i.sstatic.net/GJT6X.png" alt="Expressivness"></p>

<p>Most of the relations are relatively straight-forward. $\mathcal{L}^\omega_{\infty\omega}$ cannot express that a graph has an even number of nodes. Hence, both $\mathcal{L}_{\infty\omega}$ and $\mathcal{C}^\omega_{\infty\omega}$ are 
strictly stronger because they can express any predicate over finite structures.</p>

<p>A though one is $\mathcal{L}_{\infty\omega} \equiv \mathcal{C}_{\infty\omega}$. I think this is correct since $\mathcal{L}_{\infty\omega}$ can express every predicate, thus adding counting should not make it more powerful. This it far from a proof but at most an intuition. Any ideas?</p>

<p>The other one I don't know is $\mathcal{C}^\omega_{\infty\omega} \lneqq \mathcal{C}_{\infty\omega}$. Again my intuition is that it is correct: How can we express any predicate with finite variables even with Counting? Any ideas on that? Maybe an example which is not expressible in 
$\mathcal{C}^\omega_{\infty\omega}$?</p>

<lo.logic><descriptive-complexity><finite-model-theory>
Expressiveness of Infinitary Logic
Joachim
# Expressiveness of Infinitary Logic

(Asked by: username_0 on 2014-07-04)

I'm trying to put together a general picture of the expressiveness of some logics: First-Order Logics, Fixed-Point Logics, (Finite Variable) Infinitary Logics and the respected versions with Counting. ([Source](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.33.726))

$\mathcal{L}^k\_{\infty\omega}$ is infinitary logic with $k$ distinct variables and

$$\mathcal{L}^\omega\_{\infty\omega} := \bigcup\_{k \in \omega} \mathcal{L}^k\_{\infty\omega}$$

is finite variable infinitary logic. (Analog for Counting)

This is in the context of Finite Model Theory so in general all structures are finite.

> We say $\varphi$ and $\varphi'$ are equivalent if for every structure
> $\mathcal A$
>
> $$ \mathcal A \models\_\mathcal L \varphi \Leftrightarrow \mathcal A
> > \models\_{\mathcal {L'}} \varphi'.$$
>
> If for every $\mathcal L$-sentence there is a equivalent
> $\mathcal L'$-sentence we write
>
> $$ \mathcal L \leqq \mathcal L'.$$

![Expressivness](https://i.sstatic.net/GJT6X.png)

Most of the relations are relatively straight-forward. $\mathcal{L}^\omega\_{\infty\omega}$ cannot express that a graph has an even number of nodes. Hence, both $\mathcal{L}\_{\infty\omega}$ and $\mathcal{C}^\omega\_{\infty\omega}$ are
strictly stronger because they can express any predicate over finite structures.

A though one is $\mathcal{L}\_{\infty\omega} \equiv \mathcal{C}\_{\infty\omega}$. I think this is correct since $\mathcal{L}\_{\infty\omega}$ can express every predicate, thus adding counting should not make it more powerful. This it far from a proof but at most an intuition. Any ideas?

The other one I don't know is $\mathcal{C}^\omega\_{\infty\omega} \lneqq \mathcal{C}\_{\infty\omega}$. Again my intuition is that it is correct: How can we express any predicate with finite variables even with Counting? Any ideas on that? Maybe an example which is not expressible in
$\mathcal{C}^\omega\_{\infty\omega}$?

**Tags:** lo.logic, descriptive-complexity, finite-model-theory


---

## 1 answers

### Answer by username_1 on 2014-07-05. Score: 6 | Accepted answer

There is a famous example of [Cai, Fürer and Immerman](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.56.3003), which shows that the $\mathcal{C}\_{\infty\omega}^k$-hierarchy is strict and in particular that $\mathcal{C}\_{\infty\omega}^\omega$ cannot express every query on finite structures. The paper is quite famous because it disproved a conjecture that IFP+C captures PTIME. Your proof that $\mathcal{L}\_{\infty\omega}\equiv\mathcal{C}\_{\infty\omega}$ is correct.


---

