Separating LREC from LFP

Abstract

LREC= is an extension of frst-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-fxed-point logic with counting. We show that this containment is strict. In particular, we show that the path systems problem, a classic Pcomplete problem which is defnable in LFP-fxed-point logic-is not defnable in LREC=. This shows that the logarithmic recursion mechanism is provably weaker than general least fxed points.