Abstract: First-order logic is often portrayed as being insufficient to capture complexity classes of importance in theoretical computer science. Typically, inductive definitions such as transitive-closure are added as fixed-point operators, and the resulting logics characterize logarithmic-space computation over finite structures.
We remedy this by insisting that all structures are input in some traversal order -- one in which individual elements are related to previous elements. For example, a traversal of a connected undirected graph is a linear ordering of its vertices in which every initial segment is connected. First-order formulas invariant of the underlying traversal order are called traversal-invariant. Our results show that the traversal-invariant definitions capture logarithmic-space computability. If moreover the traversal corresponds to a breadth-first order, the breadth-first invariant elementary definitions capture nondeterministic logarithmic-space computability.
To prove these results we rely heavily on some of the most important theorems in computational complexity: the existence of universal traversal sequences; as well as the celebrated closure of nondeterministic space under complementation. Time permitting, we will discuss extensions into the transfinite.