Class Description

FO(TC): First-order with transitive closure

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 ${\displaystyle k}$ be a positive integer and ${\displaystyle u,v,x,y}$ be vectors of ${\displaystyle k}$ variables, then TC(${\displaystyle \phi _{u,v})(x,y)}$ is true if there exist ${\displaystyle n}$ variables ${\displaystyle (x_{i})}$ such that ${\displaystyle x_{1}=x,x_{n}=y}$ and for all ${\displaystyle i<n}$ ${\displaystyle \phi _{u,v}(x_{i},x_{i+1})}$. Here, ${\displaystyle \phi _{u,v}}$ is a formula over ${\displaystyle u,v}$ written in FO(TC) and ${\displaystyle \phi _{u,v}(x,y)}$ means that the variables ${\displaystyle u}$ and ${\displaystyle v}$ are replaced by ${\displaystyle x}$ and ${\displaystyle y}$.

Every formula of TC can be written in a normal form FO(${\displaystyle \phi _{u,v})(0,max)}$ where ${\displaystyle \phi }$ 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.

Linked From

FO(DTC): First-order with deterministic transitive closure

FO(DTC) is defined as FO(tc) where the transitive closure operator is deterministic, which means that when we apply DTC(${\displaystyle \phi _{u,v}}$), we know that for all ${\displaystyle u}$, there exist at most one ${\displaystyle v}$ such that phi(u,v).

We can suppose that DTC(${\displaystyle \phi _{u,v}}$) is syntactic sugar for TC(${\displaystyle \psi _{u,v}}$) where ${\displaystyle \psi (u,v)=\phi (u,v)\wedge \forall x,(x=v\vee \neg \psi (u,x))}$.

It was shown in [Imm98] on page 144 that this class is equal to L.

More about...

NL: Nondeterministic Logarithmic-Space

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 NC².

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.

More about...

SO[TC]: Second-Order logic with transitive closure

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.

More about...