Separating LREC from LFP

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. This is ongoing joint work with Anuj Dawar.

Authors

• Felipe Ferreira Santos

Keywords

No keywords are indexed for this paper.