Listings and Logics

There are standard logics DTC, TC, and LFP capturing the complexity classes L, NL, and P on ordered structures, respectively. In we have shown that LFP_inv, the "order-invariant least fixed-point logic LFP," captures P (on all finite structures) if and only if there is a listing of the P subsets of the set TAUT of propositional tautologies. We are able to extend the result to listings of the L-subsets (NL-subsets) of TAUT and the logic DTC_inv (TC_inv). As a byproduct we get that LFP_inv captures P if DTC_inv captures L. Furthermore, we show that the existence of a listing of the L-subsets of TAUT is equivalent to the existence of an almost space optimal algorithm for TAUT. To obtain this result we have to derive a space version of a theorem of Levin on optimal inverters.