You are provided with the abstract of a scientific paper and the abstracts of the papers it references. Your task is to write a Related Work section for the main paper. This section should concisely summarize and integrate the key points from the cited abstracts, reflecting how they relate to the main paper's contributions and context. In your summary, use numerical citation markers like [1], [2], etc., to refer to the corresponding papers.

Main Abstract:
The spectrum of a first-order logic sentence is the set of natural numbers that are cardinalities of its finite models. In this paper we study the hierarchy of first-order spectra based on the number of variables. It has been conjectured that it collapses to three variable. We show the opposite: it forms an infinite hierarchy. However, despite the fact that more variables can express more spectra, we show that to establish whether the class of first-order spectra is closed under complement, it is sufficient to consider sentences using only three variables and binary relations.

Cited Abstract(s):
[1]: Abstract 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 〈 B , S 〉 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 S , U 1 , …, U p such that if B is finite then 〈 B , S 〉 is a successor structure if 〈 B , S 〉 satisfies ∃ U 1 , …, ∃ U p ϕ . It implies that ⋃ NRAM( cn )=SPECTRA(∀1, unary), c ⩾1 where NRAM(cn) denotes the class of sets of positive integers accepted by a nondeterministic random access machine in time cn (where n 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.

[2]: We prove the following theorem in this paper: For any real numbers r"1, r"2, [email protected]?r"1

[3]: 

[4]: 

[5]: This paper originates from the observation that many classical NP graph problems, including some NP-complete problems, are actually of very low nondeterministic time complexity. In order to formalize this observation, we define the complexity class vertex NLIN, which collects the graph problems computable on a nondeterministic RAM in time O(n). where n is the number of vertices of the input graph G = (V.E), rather than its usual size |V| + |E|. It appears that this class is robust (it is defined by a natural restrictive computational device: it is logically characterized by several simple fragments of existential second-order logic: it is closed under various combinatorial operators, including some restrictions of transitive closure) and meaningful (if contains natural NP problems: connectivity, hamiltonicity, non-planarity, etc.). Furthermore, the very restrictive definition of vertex NLIN seems to have beneficial effects on our ability to answer difficult questions about complexity lower bounds or separation between determinism and nondeterminism. For instance, we prove that vertex NLIN strictly contains its deterministic counterpart, vertex DLIN, and even that it does not coincide with its complementary class, co-vertex NLIN. Also, we prove that several famous graph problems (e.g. planarity, 2-colourability) do not belong to vertexNLIN, although they are computable in deterministic time O(|V| - |E|).

[6]: The spectrum of a first-order sentence is the set of cardinalities of its finite models. We refine the well-known equality between the class of spectra and the class of sets (of positive integers) accepted by nondeterministic Turing machines in polynomial time. Let @math denote the class of spectra of sentences with d universal quantifiers. For any integer @math and each set of positive integers, A, we obtain: [ A NTIME (n^d ) A Sp (d ) A NTIME (n^d ( n)^2 ). ] Further the first implication holds even if we use multidimensional nondeterministic Turing machines. These results hold similarly for generalized spectra. As a consequence, we obtain a simplified proof of a hierarchy result of P. Pudlak about (generalized) spectra. We also prove that the set of primes is the spectrum of a certain sentence with only one variable.
Another body of related works is those by Grandjean, Olive and Pudlak which established the variable hierarchy for spectra of sentences using relation and function symbols [6] [3] [1] [5] [4] . Let @math denote the spectra of first-order sentences using up to @math variables with vocabulary consisting of relation and function symbols, and @math denote the restriction of @math to sentences written in prenex normal form with universal quantifiers only and using only @math variables. In his series of papers, Grandjean showed that @math , for each positive integer @math , where @math denotes the class of sets of positive integers accepted by non-deterministic RAM in time @math , and @math is the input integer [6] [3] [1] . By Skolemisation, it is shown that @math , for all @math [Theorem 3.1] GrandjeanO04 . Combined with Cook's hierarchy of non-deterministic time [2] and the known inclusions @math , for each function @math , see [3] , it implies @math , for all @math .