High-order logic is an extension of first-order and second-order with high order quantifiers. In descriptive complexity we can see that it is equal to the ELEMENTARY functions. There is a relation between the th order and non determinist algorithm the time of which is with level of exponentials.
Definitions and notations
We define high-order variable, a variable of order has got an arity and represent any set of -tuples of elements of order . They are usually written in upper-case and with a natural number as exponent to indicate the order. High order logic is the set of FO formulae where we add quantification over higher-order variables, hence we will use the terms defined in the FO article without defining them again.
HO is the set of formulae where variable's order are at most . HO is the subset of the formulae of the form where is a quantifier, means that is a tuple of variable of order with the same quantification. So it is the set of formulae with alternations of quantifiers of th order, beginning by and , followed by a formula of order .
Using the tetration's standard notation, and . with times
Every formula of th order is equivalent to a formula in prenex normal form, where we first write quantification over variable of th order and then a formula of order in normal form.
Relation to complexity classes
HO is equal to ELEMENTARY functions. To be more precise, , it means a tower of 2s, ending with where is a constant. A special case of it is that , which is exactly the Fagin's theorem. Using oracle machines in the polynomial hierarchy,