Arity hierarchies (Q2563982)

For many extensions \(L\) of first-order logic considered for finite structures there is a natural notion of arity of a formula (e.g., the maximal arity of a bounded second-order variable in a formula of fixed-point logic). Denote by \(L^k\) the fragment of \(L\) consisting of the sentences of \(L\) of arity \(\leq k\). The main lemma shows that there is a quantifier-free formula \(\varphi (x_1, \dots, x_k,y_1, \dots, y_k)\) in the language of graphs such that the transitive closure of \(\varphi\) is not expressible in \(s\text{-PFP}^{k-1}\), where \(s\text{-PFP}\) denotes simultaneous partial fixed-point logic. This result implies that the arity hierarchy (even on the class of graphs) is strict for all ``natural'' logics between transitive closure logic and \(s\text{-PFP}\) and it can be used to obtain the strictness of the corresponding hierarchies of pure DATALOG and several of its extensions and of the class of implicitly definable queries. The proof of the main lemma is based on an ingenious construction of structures ``homogeneous in the \((k-1)\)-tuples''. An iteration of this construction is needed to show the hierarchy result for deterministic transitive closure logic.