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?
We study the relationship between standard alphabets over the equality atoms, and those which can be made homogeneous using finitely many relations and functions. We leave open the problem whether these notions coincide.
We study a derivation quasi-order between between alphabets. Whenever is derived from and is non-standard then is non-standard too. We identify also a class of minimal non-standard alphabets wrt. the quasi-order.