Arity hierarchy for temporal logics (Q944387)

The paper studies the expressive power of temporal logics over trees. The main result states that in contrast to Kamp's theorem (stating, inter alia, that the temporal logic with ``Until'' and ``Since'' is expressively complete for the monadic first-order logic over the linear order of natural numbers), for every \(n\) there is a modality of arity \(n\) definable by a monadic logic formula, which is not equivalent over trees to any temporal logic formula which uses modalities of arity less than \(n\). The proof uses an instance of Shelah's composition theorem. Interesting corollaries of this result are, e.g., new proofs that CTL* and ECTL+ have no finite bases.