First-order spectra with one variable

Define a (∀1 unary)-sentence to be a prenex first-order sentence of unary type (i.e., a type which only contains unary relation and function symbols and constant symbols) with only one (universal) quantifier. A successor structure is a structure 〈, 〉 such that S is a function which is a permutation of the basis B with only one cycle. We exhibit a (∀1, unary)-sentence φ of type {, , …, } such that if is finite then 〈, 〉 is a successor structure if 〈, 〉 satisfies ∃, …, ∃. It implies that ⋃ NRAM()=SPECTRA(∀1, unary), ⩾1 where NRAM(cn) denotes the class of sets of positive integers accepted by a nondeterministic random access machine in time (where is the input integer) and SPECTRA(∀1, unary) is the class of finite spectra of (∀1, unary)-sentences. Another consequence is that some graph properties (hamiltonicity, connectedness) can be characterised by sentences with unary function symbols and constant symbols and only one variable. This contrasts with the result (by Fagin and De Rougemont) that these two graph properties are not definable by monadic generalized spectra (without function symbols) even in the presence of an underlying successor relation.