HO (complexity)


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

Property

Normal form

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 NP |, which is exactly the Fagin's theorem. Using oracle machines in the polynomial hierarchy, NTIME|