Grohe and Schweikardt proved in 2005 that the smallest sentence of 3-variable logic FO^3^ that can separate a linear order of length n from all shorter linear orders is of length at least O(√n). The best upper bound for the length of such a sentence that we found in the literature is O(n).
In this talk I present a new game that characterizes definability by sentences of FO^k^ with n quantifiers. Using this game I show that there is a sentence of FO^3^ with 2m+1 quantifiers that is true in a linear order if and only if its length is at least 2m(m+1)+1. Furthermore, I show a matching lower bound result using the game: all linear orders of length at least 2m(m+1)+1 are equivalent with respect to all sentences of FO^3^ with at most 2m+1 quantifiers. The first of these results implies O(√n) upper bound for the length of a sentence of FO^3^ needed for separating linear orders of length n from shorter linear orders.
(joint work with Kerkko Luosto)
