## $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 2011 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 ## 1 Answer 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. – Frank Apr 21 2011 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). – Frank Apr 22 2011 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 2011 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? – Frank Apr 23 2011 at 4:49