一句话：简化证明 Stavi 定理：Until、Since 与 Stavi 模态的时序逻辑在所有线性序上表达力等价于 FOMLO。
Kamp 定理表明，带 Until 与 Since 的时序逻辑在 Dedekind 完备时间流上和一阶一元序逻辑（FOMLO）表达力等价，但在有理数等线性序上并不完备。Stavi 为此引入两个额外模态，并证明在 Until、Since 与 Stavi 模态共同存在时，该时序逻辑在所有线性序上都与 FOMLO 表达力等价。本文重新给出 Stavi 定理的一个简单证明，目标是以更简洁的方式论证这一表达等价性。论文属于理论逻辑研究，不涉及实现或实验评估，其贡献主要在于提供更清晰、易验证的证明。
Kamp's theorem established the expressive equivalence of the temporal logic with Until and Since and the First-Order Monadic Logic of Order (FOMLO) over the Dedekind-complete time flows. However, this temporal logic is not expressively complete for FOMLO over the rationals. Stavi introduced two additional modalities and proved that the temporal logic with Until, Since and Stavi's modalities is expressively equivalent to FOMLO over all linear orders. We present a simple proof of Stavi's theorem.Comment: arXiv admin note: text overlap with arXiv:1401.2580