一句话：证明正一阶逻辑 FO+ 在有限词与图上表达力受限：Lyndon 保持定理失效，且正则语言的 FO+ 可定义性不可判定。
论文研究 FO+：有限词上的一阶逻辑片段，其中一元谓词只能以肯定形式出现。作者构造了一个在一元谓词上单调、可由 FO 定义却不能在 FO+ 中定义的语言，由此给出 Lyndon 保持定理在有限结构上不成立的简单证明。该反例被提升到有限图，说明即使图类对加边封闭，仍可能需要否定才能用 FO 定义。最后，论文证明判定给定有限词正则语言是否 FO+ 可定义是不可判定的。这些结果刻画了正性与有限模型/图封闭性之间的张力，并给出 FO+ 表达力与判定性的边界。
We study FO+, a fragment of first-order logic on finite words, where monadic predicates can only appear positively. We show that there is an FO-definable language that is monotone in monadic predicates but not definable in FO+. This provides a simple proof that Lyndon's preservation theorem fails on finite structures. We lift this example language to finite graphs, thereby providing a new result of independent interest for FO-definable graph classes: negation might be needed even when the class is closed under addition of edges. We finally show that the problem of whether a given regular language of finite words is definable in FO+ is undecidable.