The Descriptive Complexity of Decision Problems through Logics with Relational Fixed-Point and Capturing Results

In this work, we generalize the classical fixed-point logics using relations instead of operators in order to capture the notion of nondeterminism. The basic idea is that we use loops in a relation instead of fixed-points of a function, that is, X is a fixed-point of the relation R in case the pair (X,X) belongs to R. We introduce the notion of initial fixed-point of an inflationary relation R and the associated operator rifp. We denote by RIFP the first-order logic with the inflationary relational fixed-point operator rifp and show that it captures the polynomial hierarchy using a translation to second-order logic. We also consider the fragment RIFP1 with the restriction that the rifp operator can be applied at most once. We show that RIFP1 captures the class NP and compare our logic with the nondeterministic fixed-point logic proposed by Abiteboul, Vianu and Vardi in [S. Abiteboul, M. Vardi, and V. Vianu. Fixpoint logics, relational machines, and computational complexity. Journal of the ACM, 44-1:30-56, 1997].