The ordered fragment of first-order logic is a set of formulas where variables always occur in atoms in a fixed order, which is also the order in which they are to be quantified. Its origin can be traced back to W. V. Quine's work on predicate functor logic, while the formal definition and the term 'ordered formulas' were established by A. Herzig. Herzig proposed a translation from ordered formulas to modal formulas and showed that satisfiability is invariant under the translation, provided that the modal satisfaction in consideration is that of \(\mathbf{KD}\). Thus, the satisfiability problem for ordered formulas is decidable.

In this talk I introduce the ordered fragment defined by Herzig, and present a simplified proof of his result and the computational complexity of the satisfiability problem. The proof relies on a technique for deriving tree-like Kripke structures from first-order structures and vice versa. I also discuss the expressive power of the fragment based on a recent work by B. Bednarczyk and R. Jaakkola, and show that a bisimulation (for the ordered fragment) between two first-order structures induces a modal bisimulation between the corresponding Kripke structures.