Editing Descriptive complexity theory (section)

=== 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>