The fluted fragment with transitive relations (Q2238133)

This is a technical paper focused on a fragment of first-order logic called \emph{fluted} and characterized by a restriction on the occurrences of object variables. In a nutshell, variables can be indexed by natural numbers, they must occur ordered and without gaps in every atom, composed formulas must share the variable of highest index, and quantified variables must have the highest indices in the associated immediate subformulas. For example, \[ \forall x_1 (\text{person }(x_1) \rightarrow \exists x_2\text{ has parent }(x_1,x_2)) \] is a statement in the fluted fragment of first-order logic, while \[ \forall x_1 (\text{person }(x_1) \rightarrow \exists x_2\text{ is parent of }(x_2,x_1)) \] is not (because variables in \(\text{is parent of }(x_2,x_1)\) are not ordered). An interesting property of the fluted fragment is that its satisfiable formulas are guaranteed to have some finite models, a property known as \emph{finite model property}. The paper considers a few extensions of the fragment and formally establishes that such a property is lost if the language permits the usage of equality and transitive relations. All results are described in easy-to-understand terms, as well as with rigour and detailed proofs. A few figures help to visualize some technical constructions. Whether the finite model property is lost in presence of transitive relations without the usage of equality is left open, but some interesting directions are given in the concluding section.