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 given a regular language of finite words, it is undecidable whether it is definable in FO+.

翻译：我们研究FO+,这是关于限定词的一阶逻辑的片段,在限定词上,monadic 的前提只能出现正面。我们显示有一种FO可定义的语言,在monadic 的前提中是单调的,但在FO+中是无法定义的。这简单证明Lyndon的保存定理在限定结构上失败了。我们将这一示例语言移到限定图中,从而为FO可定义的图表类别提供了一种独立利益的新结果:即使该类在加边线下关闭,也可能需要否定。我们最后显示,如果有固定的限定词语言,那么在FO+中是否可定义是不可量化的。