一句话：给出 Lyndon 保持定理在有限结构上失败的简单证明，并证明正则语言的 FO+ 可定义性不可判定。
本文研究有限字上的一阶逻辑片段 FO+，其中一元谓词只能以正出现的方式使用。作者构造了一个在 FO 中可定义、且对一元谓词单调的语言，证明它不能用 FO+ 定义。这一结果说明 Lyndon 保持定理在有限结构上不再成立，并给出了一个简单的反例证明。此外，论文还考察 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 additionally show that given a regular language, it is undecidable whether it is definable in FO+.