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 Th k loc ( λ, 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 ∧ ψ > 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.

Authors

• Ryan Siders

Keywords

• Decidability
• Complete theories
• Finite axiomatizabilty
• Semimodel
• Linear order
• Ehrenfeucht–Fraïssé game