Editing Descriptive complexity theory (section)

==Elementary functions==
The [[time complexity]] class [[ELEMENTARY]] of elementary functions can be characterised by '''HO''', the [[complexity class]] of structures that can be recognized by formulas of [[higher-order logic]]. Higher-order logic is an extension of [[first-order logic]] and [[second-order logic]] with higher-order quantifiers.  There is a relation between the <math>i</math>th order and non-deterministic algorithms the time of which is bounded by <math>i-1</math> levels of exponentials.<ref>{{Cite journal| first1 = Lauri|last1= Hella|first2 = José María|last2 = Turull-Torres | title =Computing queries with higher-order logics | journal =Theoretical Computer Science | volume = 355 | issue = 2 | year = 2006 | pages = 197–214   | issn =0304-3975 | publisher =Elsevier Science Publishers Ltd. | place =  Essex, UK | doi=10.1016/j.tcs.2006.01.009| doi-access = free }}</ref>

=== Definition ===
We define higher-order variables. A variable of order <math>i>1</math> has an arity <math>k</math> and represents any set of <math>k</math>-[[tuple]]s of elements of order <math>i-1</math>. They are usually written in upper-case and with a natural number as exponent to indicate the order. Higher-order logic is the set of first-order  formulae where we add quantification over higher-order variables; hence we will use the terms defined in the [[FO (complexity)|FO]] article without defining them again.

HO<math>^i</math> is the set of formulae with variables of order at most <math>i</math>. HO<math>^i_j</math> is the subset of formulae of the form <math>\phi=\exists \overline{X^i_1}\forall\overline{X_2^i}\dots Q \overline{X_j^i}\psi</math>, where <math>Q</math> is a quantifier and <math>Q \overline{X^i}</math> means that <math>\overline{X^i}</math> is  a tuple of variable of order <math>i</math> with the same quantification. So HO<math>^i_j</math> is the set of formulae with <math>j</math> alternations of quantifiers of order <math>i</math>, beginning with <math>\exists</math>, followed by a formula of order <math>i-1</math>.

Using the standard notation of the [[Tetration#Notation|tetration]], <math>\exp_2^0(x)=x</math> and <math> \exp_2^{i+1}(x)=2^{\exp_2^{i}(x)}</math>. <math> \exp_2^{i+1}(x)=2^{2^{2^{2^{\dots^{2^{x}}}}}}</math> with <math>i</math> times <math>2</math>

=== Normal form ===
Every formula of order <math>i</math>th  is equivalent to a formula in prenex normal form, where we first write quantification over variable of <math>i</math>th order and then a formula of order <math>i-1</math> in normal form.

=== Relation to complexity classes ===
HO is equal to the class [[ELEMENTARY]] of elementary functions.  To be more precise, <math>\mathsf{HO}^i_0 = \mathsf{NTIME}(\exp_2^{i-2}(n^{O(1)}))</math>, meaning a tower of <math>(i-2)</math>  2s, ending with <math>n^c</math>, where <math>c</math> is a constant. A special case of this is that [[NP (complexity)|<math>\exists\mathsf{SO}=\mathsf{HO}^2_0=\mathsf{NTIME}(n^{O(1)})={\color{Blue}\mathsf{NP}}</math>]], which is exactly [[Fagin's theorem]]. Using [[oracle machine]]s in the [[polynomial hierarchy]], [[NTIME|<math>\mathsf{HO}^i_j={\color{Blue}\mathsf{NTIME}}(\exp_2^{i-2}(n^{O(1)})^{\Sigma_j^{\mathsf P}})</math>]]