# 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 $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$_{j}^{i}$ is the subset of the formulae of the form $\phi =\exists {\overline {X_{1}^{i}}}\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, ${\mathsf {HO}}_{0}^{i}={\mathsf {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 {\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, ${\mathsf {HO}}_{j}^{i}={\color {Blue}{\mathsf {NTIME}}}(\exp _{2}^{i-2}(n^{O(1)})^{\Sigma _{j}^{\mathsf {P}}})$ 