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 $i$th order and non determinist algorithm the time of which is with $i-1$ level of exponentials.

Definitions and notations

We define high-order variable, a variable of order $i>1$ has got an arity $k$ and represent any set of $k$-tuples of elements of order $i-1$. 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$^i$ is the set of formulae where variable's order are at most $i$. HO$^i_j$ is the subset of the formulae of the form $\phi=\exists \overline{X^i_1}\forall\overline{X_2^i}\dots Q \overline{X_j^i}\psi$ where $Q$ is a quantifier, $Q \overline{X^i}$ means that $\overline{X^i}$ is a tuple of variable of order $i$ with the same quantification. So it is the set of formulae with $j$ alternations of quantifiers of $i$th order, beginning by and $\exists$, followed by a formula of order $i-1$.

Using the tetration's standard notation, $\exp_2^0(x)=x$ and $\exp_2^{i+1}(x)=2^{\exp_2^{i}(x)}$. $\exp_2^{i+1}(x)=2^{2^{2^{2^{\dots^{2^{x}}}}}}$ with $i$ times $2$

Property

Normal form

Every formula of $i$th order is equivalent to a formula in prenex normal form, where we first write quantification over variable of $i$th order and then a formula of order $i-1$ in normal form.

Relation to complexity classes

HO is equal to ELEMENTARY functions. To be more precise, $\text{HO}^i_0 = \text{NTIME}(\exp_2^{i-2}(n^{O(1)}))$, it means a tower of $(i-2)$ 2s, ending with $n^c$ where $c$ is a constant. A special case of it is that $\exists{}SO$=HO$^2_0$=NTIME($n^{O(1)}$)=NP, which is exactly the Fagin's theorem. Using oracle machines in the polynomial hierarchy, HO$^i_j$=NTIME($\exp_2^{i-2}(n^{O(1)})^{\Sigma_j^{\rm P}}$)

References

1. 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

External links

• zoo about HO.