The uniform one-dimensional fragment of first-order logic was introduced a few years ago as a generalization of the two-variable fragment to contexts involving relations of arity greater than two. Quantifiers in this logic are used in blocks, each block consisting only of existential quantifiers or only of universal quantifiers. In this paper we consider the possibility of mixing both types of quantifiers in blocks. We show the finite (exponential) model property and NExpTime-completeness of the satisfiability problem for two restrictions of the resulting formalism: in the first we require that every block of quantifiers is either purely universal or ends with the existential quantifier, in the second we restrict the number of variables to three; in both equality is not allowed. We also extend the second variation to a rich subfragment of the three-variable fragment (without equality) that still has the finite model property and decidable, NExpTime{}-complete satisfiability.

翻译：均匀一阶逻辑片段是数年前作为二元关系片段向多元关系（元数大于二）情境的推广而引入的。该逻辑中量词以块的形式使用，每个块只包含存在量词或只包含全称量词。本文研究了在量词块中混合使用两种量词类型的可能性。我们证明了两种受限形式化系统的有限（指数）模型性质及可满足性问题的NExpTime完全性：第一种要求每个量词块要么是全称量词块，要么以存在量词结尾；第二种将变量数量限制为三个；两种情形均不包含等式。此外，我们将第二种变体推广至三变量片段（不含等式）的丰富子片段，该子片段仍保持有限模型性质及可判定的NExpTime完全可满足性。