Separating LREC from LFP

TL;DR

This paper demonstrates that the logic LREC= is strictly less expressive than fixed-point logic with counting by proving the inexpressibility of the path systems problem within LREC= using a novel game approach.

Contribution

It introduces a new Spoiler-Duplicator game to analyze the expressive power of LREC= and establishes its limitations compared to fixed-point logic with counting.

Findings

LREC= is contained in FPC but is strictly weaker.

The path systems problem is not definable in LREC=.

A novel game method is developed to prove inexpressibility results.

Abstract

LREC= is an extension of first-order logic with a logarithmic recursion operator. It was introduced by Grohe et al. and shown to capture the complexity class L over trees and interval graphs. It does not capture L in general as it is contained in FPC - fixed-point logic with counting. We show that this containment is strict. In particular, we show that the path systems problem, a classic P-complete problem which is definable in LFP - fixed-point logic - is not definable in LREC= This shows that the logarithmic recursion mechanism is provably weaker than general least fixed points. The proof is based on a novel Spoiler-Duplicator game tailored for this logic.