The quantifier structure of sentences that characterize nondeterministic time complexity

The well-known model theoretic characterization of nondeterministic time complexity is studied. It is shown that for every nondeterministic Turing machine M of time complexity T(n), there is an existential second-order sentence σ of a very restricted form, whose set of finite models corresponds to the set of strings recognized by M. Specifically, σ is in the theory of addition restricted to finite segments of the natural numbers. Also, for every string x accepted by M, the length of the encoding of the model corresponding to x is O(T(|x|)). A consequence is that if T(n)=n^d, then an upper bound is obtained for the degree of the second-order variables of σ. Potential applications to low-level complexity are discussed