A logic with temporally accessible iteration

TL;DR

This paper introduces a unifying logical framework called FO+TAI that integrates fixed point operators with temporal logic, showing it subsumes many fixed point logics but has equivalent expressive power to FO+PFP over finite structures.

Contribution

The paper presents a new logic with iteration operator that unifies various fixed point logics and analyzes its expressive power compared to existing logics.

Findings

FO+TAI subsumes all fixed point extensions as fragments.

Over finite structures, FO+TAI is equally expressive as FO+PFP.

Adding iteration to FO+LFP does not increase its expressive power.

Abstract

Deficiency in expressive power of the first-order logic has led to developing its numerous extensions by fixed point operators, such as Least Fixed-Point (LFP), inflationary fixed-point (IFP), partial fixed-point (PFP), etc. These logics have been extensively studied in finite model theory, database theory, descriptive complexity. In this paper we introduce unifying framework, the logic with iteration operator, in which iteration steps may be accessed by temporal logic formulae. We show that proposed logic FO+TAI subsumes all mentioned fixed point extensions as well as many other fixed point logics as natural fragments. On the other hand we show that over finite structures FO+TAI is no more expressive than FO+PFP. Further we show that adding the same machinery to the logic of monotone inductions (FO+LFP) does not increase its expressive power either.