On quantifier-rank equivalence between linear orders

We construct winning strategies for both players in the Ehrenfeucht–Fraïssé game on linear orders. To this end, we define the local quantifier-rank k theory of a linear order with a single constant (λ,x), and prove a normal form for ≡k classes, expressed in terms of local classes. We describe two implications of this theorem: 1. a decision procedure for whether a set U of pairs of ≡k classes is consistent – whether for some linear order λ, U is the set of pairs (ϕ,ψ) such that λ⊨∃x(ϕx) – which runs in time linear in the size of the formula which expresses that exactly the pairs of ≡k classes in U are realized. The only obstacle to effectively listing the theory of linear order is the vast number of different ≡k classes of theories of linear order. 2. We find a finitely axiomatizable linear order λ which we construct inside any ≡k class of linear orders. We relate our winning strategies to semimodels of the theory of linear order. First, we situate our result in a historical background.