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.[1] 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 , which is exactly the Fagin's theorem. Using oracle machines in the polynomial hierarchy,
References
- ↑ Lauri Hella and José María Turull-Torres (2006), "Computing queries with higher-order logics", Theoretical Computer Science ((what is called "number" in bibtex) ed.), Essex, UK: Elsevier Science Publishers Ltd., 355 (2): 197–214, doi:10.1016/j.tcs.2006.01.009, ISSN 0304-3975