Three Variables Suffice for Real-Time Specification

TL;DR

This paper proves that the ordered real line with the unary +1 function can be fully described using only three variables in monadic first-order logic, simplifying real-time specification tasks.

Contribution

It establishes the 3-variable property for the structure $( eal, <, +1)$ and related structures, advancing understanding of variable requirements in real-time logic specifications.

Findings

$( eal, <, +1)$ has the 3-variable property.

The 3-variable property extends to $( eal, <, f)$ for any fixed linear function $f$.

Counterexample shows some countable dense orders lack the $k$-variable property for any $k$.

Abstract

A natural framework for real-time specification is monadic first-order logic over the structure $(\mathbb{R},<,+1)$---the ordered real line with unary $+1$ function. Our main result is that $(\mathbb{R},<,+1)$ has the 3-variable property: every monadic first-order formula with at most 3 free variables is equivalent over this structure to one that uses 3 variables in total. As a corollary we obtain also the 3-variable property for the structure $(\mathbb{R},<,f)$ for any fixed linear function $f:\mathbb{R}\rightarrow\mathbb{R}$. On the other hand, we exhibit a countable dense linear order $(E,<)$ and a bijection $f:E\rightarrow E$ such that $(E,<,f)$ does not have the $k$-variable property for any $k$.