一句话：证明有限结构上双向互模拟不变的一元最小不动点逻辑恰好对应双向 μ-演算。
van Benthem 曾用模态逻辑刻画一阶逻辑（FOL）的互模拟不变片段，Janin 与 Walukiewicz 则用 μ-演算刻画一元二阶逻辑（MSO）的相应片段，但这些论证不能直接推广到有限结构；FOL 情形虽有 Rosen 的替代证明，比 FOL 更强的逻辑在有限结构上的类似刻画仍是长期未解问题。本文针对介于 FOL 与 MSO 之间的无参数一元最小不动点逻辑证明此类刻画：在有限结构上，该逻辑中每个双向互模拟不变公式都等价于双向 μ-演算公式，反之亦然。
A seminal theorem by van Benthem characterises the bisimulation-invariant fragment of First Order Logic (FOL) in terms of Modal Logic. Similarly, Janin and Walukiewicz have shown that the bisimulation-invariant fragment of Monadic Second Order Logic (MSO) corresponds precisely to the (modal) mu-calculus. Notably, neither argument immediately carries over when only considering finite structures. In the case of FOL, Rosen provided an alternative proof, which also works over finite structures. However, such characterisations for any logic more expressive than FOL over finite structures have remained long-standing open problems. In this paper, we prove such a characterisation for parameter-free Monadic Least Fixpoint Logic, a well-known logic in between FOL and MSO. In particular, we show that, over finite structures, every two-way bisimulation-invariant formula in this logic is equivalent to a formula in the two-way mu-calculus and vice versa.
@inproceedings{PfluegerMK24,
title = {A Characterisation Theorem for Two-Way Bisimulation-Invariant Monadic Least Fixpoint Logic Over Finite Structures},
author = {Maximilian Pflueger and Johannes Marti and Egor V. Kostylev},
booktitle = {LICS},
year = {2024},
doi = {10.1145/3661814.3662107}
}