FO(TC) is the set of boolean queries definable with first-order formulae with a transitive closure (TC) operator.
TC is defined this way: let be a positive integer and be vectors of variables, then TC( is true if there exist variables such that and for all . Here, is a formula over written in FO(TC) and means that the variables and are replaced by and .
Every formula of TC can be written in a normal form FO( where is a FO formula and we suppose that there is an order on the model where variables are quantified, so we can choose the minimum and maximum element.
It was shown in [Imm98] page 150 that this class is equal to NL.
FO(DTC) is defined as FO(tc) where the transitive closure operator is deterministic, which means that when we apply DTC(), we know that for all , there exist at most one such that phi(u,v).
We can suppose that DTC() is syntactic sugar for TC() where .
It was shown in [Imm98] on page 144 that this class is equal to L.
NL is to L as NP is to P. Not known whether a particular relation (equality or inequality) between P and NP implies the same relation between L and NL.
In a breakthrough result, was shown to equal coNL [Imm88] [Sze87]. (Though contrast to mNL.)
Is contained in LOGCFL [Sud78], as well as NC2.
Is contained in UL/poly [RA00].
Deciding whether a bipartite graph has a perfect matching is hard for NL [KUW86].
NL can be defined in a logical formalism as SO(krom) and also as FO(tc), reachability in directed graph is NL-Complete under FO-reduction.
SO[TC] is to SO as FO[TC] is to FO. The TC operator can now also take second-order variable as argument.
In Descriptive complexity we can see thatSO[TC] is equal to PSPACE.