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

Definitions and notations

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

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

Property

Normal form

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

Relation to complexity classes

HO is equal to ELEMENTARY functions. To be more precise, ${\displaystyle {\mathsf {HO}}_{0}^{i}={\mathsf {NTIME}}(\exp _{2}^{i-2}(n^{O(1)}))}$, it means a tower of ${\displaystyle (i-2)}$ 2s, ending with ${\displaystyle n^{c}}$ where ${\displaystyle c}$ is a constant. A special case of it is that ${\displaystyle \exists {\mathsf {SO}}={\mathsf {HO}}_{0}^{2}={\mathsf {NTIME}}(n^{O(1)})={\color {Blue}{\mathsf {NP}}}}$, which is exactly the Fagin's theorem. Using oracle machines in the polynomial hierarchy, ${\displaystyle {\mathsf {HO}}_{j}^{i}={\color {Blue}{\mathsf {NTIME}}}(\exp _{2}^{i-2}(n^{O(1)})^{\Sigma _{j}^{\mathsf {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.