# $2$-variable segment of FO over ordered, finite structures

Let $FO$ be first-order logic and $FO^k$ be $k$-variable segment of $FO$, i.e. $FO^k$ has only $k$ variables.

To my understanding, for every sentence $\varphi\in FO$ there exists a sentence $\psi\in FO^2$ such that for all finite structures $\mathfrak{A}$ with linear order it is the case that $\mathfrak{A}\vDash\varphi$ iff $\mathfrak{A}\vDash\psi$.

Is this true? Are there any assumptions about the vocabulary?

-
Are you sure you can express a sentence like "there are at least three elements" using only two variables? –  boumol Apr 20 '11 at 13:57
@boumol: Re-use of variables is permitted, so, thanks to the order, one can express "there are at least three elements" as $\exists x\exists y (x<y \land \exists x(y<x))$. –  Andreas Blass Apr 20 '11 at 15:29
OK, this proposal seems to work (under the consideration that "ordered" means "linearly ordered"). I didn't think that the order would help to write down this property (without the order I would guess the answer is no), but it really helps. –  boumol Apr 20 '11 at 15:43
@bournol: Yes, the order is indeed linear, I will edit to include that. Thanks for pointing it out. –  user10891 Apr 20 '11 at 16:56
If the statement holds true when the language contains a ternary operation or relation symbol, I will be surprised. Gerhard "Ask Me About System Design" Paseman, 2011.04.20 –  Gerhard Paseman Apr 20 '11 at 17:04

It is not the case. As an example, the following paper:

Kouck´y, M., Lautemann, C., Poloczek, S., Th´erien, D.: Circuit lower bounds via Ehrenfeucht-Fraiss´e games, 2006.

shows that, over words, FO[+, $\times$] with 2 variables is equivalent to AC$^0$ with linear size circuits --- while FO[+, $\times$] is equivalent to the whole class AC$^0$.

Those two classes are known to differ (S. Chaudhuri and J. Radhakrishnan: Deterministic restrictions in circuit complexity, 1996).

-
Thanks for the pointers, I will study those papers more closely during weekend. –  user10891 Apr 21 '11 at 4:21
I guess I'm missing something here. It seems $FO(all)\subset AC^0$ where $AC^0$ is polysize and constant depth and $FO(all)$ is $FO$ with arbitrary numerical predicates, but $FO(all)$ can express non-computable queries. If $FO(+,\times) = AC^0$, then $FO(+,\times)$ could also express non-computable queries? This seems a contradiction, thus I'm likely missing something. (There are some cases where a property expressible by a sequence $\varphi_i$ of $FO$-sentences, where each $\varphi$ has a bounded number of quantifiers, is equivalent to $AC^0$, but I haven't yet studied this direction). –  user10891 Apr 22 '11 at 11:39
You're missing the crucial notion of <i>uniformity</i>: the computational power needed to generate the circuit for each input size. FO(all) (usually denoted FO[$\mathcal{N}$] or FO[$\mathfrak{Arb}$]) equals <i>non-uniform</i> AC$^0$, which includes non-decidable languages (for instance, any unary language is in AC$^0$). FO[+, $\times$] corresponds to a nicer (more realistic) notion of uniformity (namely, logtime-uniform). A nice survey on this topic is given by Schweikardt. –  Michaël Apr 23 '11 at 2:11
@Michaël, thanks! This clarifies the situation and I'm back to work. I will accept your answer now that I start to understand it :) Btw, do you happen to know if its possile to this with 3 variables? –  user10891 Apr 23 '11 at 4:49