A result of Grädel and McColm shows that over finite structures, the logic DTCL is strictly less expressive than the logic TCL. My question is: can this result be translated into some separation result concerning Turing machines with atoms?

TCL is first-order logic extended by the transitive closure operator – which allows to define the transitive closure of a relation of arity defined earlier, where is treated as a binary relation over -tuples. DTCL is similar, except for that the operator only works if the relation is a partial function (i.e., is deterministic); otherwise the operator returns the empty relation.

Note that over linearly ordered structures, the logic TCL captures NL, while DTCL captures L. In particular, it is not known whether the two logics are equivalent over finite structures equipped with a linear order. However, it is known that in general, they are not equivalent:

Theorem (Grädel and McColm). Over the class of all finite structures, DTCL is strictly less expressive than TCL, i.e., there is a property of finite structures which is expressible in TCL but not in DTCL.

This property is graph connectedness, which is clearly expressible in TCL. To show  that it is not expressible in DTCL, one uses the following argument.

For a graph , let denote the graph with vertex set , and edges are where and . One then shows that over graphs of the form , the logic DTCL collapses to FO logic, and FO logic cannot determine connectedness. For a tuple of elements vertices of , let denote the set . Because any bijection of leaving the first component of each vertex fixed is an automorphism of , it is easy to see that no deterministic path starting from can leave the set , so has length bounded by some number , where depends only on , and not on the graph . Therefore, the DTCL operator can be replaced by a FO formula (by an -fold expansion of the transitive closure).

The question is: does this argument give some separation result for Turing Machines with Atoms? For example, that L and NL are different, over some alphabets? And is there a notion of a standard alphabet suited for L?

Edit.

I think that the right notion of a -standard alphabet is as follows. Let be a complexity class with atoms. An alphabet is -standard if over the alphabet , the class doesn’t increase in power after extending it by the choice oracle – an oracle which, for a given letter provides a tuple of atoms supporting it, of bounded length (the machine equipped with the oracle should accept or not regardless of the choices made by the oracle, similarly as in order-invariant Turing machines).

The notion of a standard alphabet (over equality atoms) which we considered earlier is the same thing as the notion of a Det-standard alphabet, or, as it turns out, as the notion of a P-standard alphabet, according to the above definition. The notion of a Log-standard alphabet also makes sense, and it is not clear – as Mikołaj mentions in the comment – whether this notion is equivalent  standardness. Also, it is not clear what the definition of a LogSpace machine with atoms should be: in one definition, the auxiliary tapes can store log-many symbols from an orbit-finite alphabet, and in another definition – from a finite alphabet. I think that the construction from the  Gradel-McColm theorem might provide an example of an alphabet which is standard but not Log-standard, for one of the two definitions of the class LogSpace.