A Proof of Stavi's Theorem

TL;DR

This paper provides a simple proof of Stavi's theorem, showing that adding Stavi's modalities to temporal logic achieves expressive equivalence with First-Order Monadic Logic of Order over all linear orders.

Contribution

The paper offers a straightforward proof of Stavi's theorem, extending the understanding of temporal logic's expressive power with new modalities.

Findings

Temporal logic with Stavi's modalities is equivalent to FOMLO over all linear orders.

A simplified proof of Stavi's theorem is presented.

The result extends the expressive completeness of temporal logic beyond Kamp's theorem.

Abstract

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.