The uniform one-dimensional fragment of first-order logic was introduced a few years ago as a generalization of the two-variable fragment of first-order logic 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 quantifiers in blocks. We identify a non-trivial variation of the logic with mixed blocks of quantifiers which retains some good properties of the two-variable fragment and of the uniform one-dimensional fragment: it has the finite (exponential) model property and hence decidable, NExpTime-complete satisfiability problem.
翻译:一阶逻辑的统一一维片段于数年前被提出,作为一阶逻辑两变量片段在涉及大于二元关系语境中的推广。该逻辑中的量词以块形式使用,每个块仅由存在量词或仅由全称量词构成。本文探讨了在量词块中混合量词的可能性。我们识别出一种带有混合量词块、保留了两变量片段与统一一维片段良好性质的非平凡逻辑变体:该变体具有有限(指数)模型性质,因此其可满足性问题是可判定的,且为NExpTime完全问题。