一句话:证明 FO[A_RB] 与 FO[≤, MSB0, F_IN] 等表达,且 FO[≤, F_IN] 和 FO[≤, MSB0] 满足强 Crane Beach 性质。
该论文研究词上的一阶逻辑(FO)在数值谓词扩展下的表达力与 Crane Beach 性质(CBP)。作者证明 FO[A_RB] 与仅含序、二元 MSB0 谓词和有限度谓词的 FO[≤, MSB0, F_IN] 等表达。CBP 要求所有含中性字母的可表达语言都是正则的;已知 FO[A_RB] 不满足 CBP,但本文证明 FO[≤, F_IN] 与 FO[≤, MSB0] 满足强 CBP。因此 FO[≤, F_IN] 同时具有局部性和 CBP,能表达大量语言,却仅比 FO[A_RB] 少一个简单谓词。最后将其计数能力作为应用进行了研究。
First-order logic (FO) over words is shown to be equiexpressive with FO equipped with a restricted set of numerical predicates, namely the order, a binary predicate MSB<inf>0</inf>, and the finite-degree predicates: FO[A<inf>RB</inf>] = FO[≤, MSB<inf>0</inf>, F<inf>IN</inf>]. The Crane Beach Property (CBP), introduced more than a decade ago, is true of a logic if all the expressible languages admitting a neutral letter are regular. Although it is known that FO[A<inf>RB</inf>] does not have the CBP, it is shown here that the (strong form of the) CBP holds for both FO[≤, F<inf>IN</inf>] and FO[≤, MSB<inf>0</inf>]. Thus FO[≤, F<inf>IN</inf>] exhibits a form of locality and the CBP, and can still express a wide variety of languages, while being one simple predicate away from the expressive power of FO[A<inf>RB</inf>]. The counting ability of FO[≤, F<inf>IN</inf>] is studied as an application.