We study the positive logic FO+ on finite words, and its fragments, pursuing and refining the work initiated in [Kuperberg 2023]. First, we transpose notorious logic equivalences into positive first-order logic: FO+ is equivalent to LTL+ , and its two-variable fragment FO2+ with (resp. without) successor available is equivalent to UTL+ with (resp. without) the "next" operator X available. This shows that despite previous negative results, the class of FO+-definable languages exhibits some form of robustness. We then exhibit an example of an FO-definable monotone language on one predicate, that is not FO+-definable, refining the example from [Kuperberg 2023] with 3 predicates. Moreover, we show that such a counter-example cannot be FO2-definable.
翻译:本文研究有限词上的正一阶逻辑FO+及其片段,延续并深化了[Kuperberg 2023]中开启的研究工作。首先,我们将若干经典逻辑等价关系移植到正一阶逻辑框架中:FO+等价于LTL+,而其带(或不带)后继关系的二变元片段FO2+分别等价于带(或不带)“下一个”算子X的UTL+。这表明尽管存在先前的否定性结论,FO+可定义语言类仍展现出某种鲁棒性。随后,我们构造了一个在单一谓词上可被FO定义但不可被FO+定义的单调语言实例,从而将[Kuperberg 2023]中基于三个谓词的示例进行了精细化。此外,我们证明此类反例不可能被FO2逻辑所定义。