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

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$.
• 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