Samiksha Jaiswal (Editor) I am a computer expert who loves a challenge. When I am not managing servers and fixing flaws, I write about it and other interesting things on various blogs.
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 ith order and non determinist algorithm the time of which is with i−1 level of exponentials.
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.
HOi is the set of formulae where variable's order are at most i. HOji is the subset of the formulae of the form ϕ=∃X1i¯∀X2i¯…QXji¯ψ where Q is a quantifier, QXi¯ means that Xi¯ 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 ith order, beginning by and ∃, followed by a formula of order i−1.
Using the tetration's standard notation, exp20(x)=x and exp2i+1(x)=2exp2i(x). exp2i+1(x)=2222…2x with i times 2
Normal form
Every formula of ith order is equivalent to a formula in prenex normal form, where we first write quantification over variable of ith 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, HO0i=NTIME(exp2i−2(nO(1))), it means a tower of (i−2) 2s, ending with nc where c is a constant. A special case of it is that ∃SO=HO02=NTIME(nO(1))=NP, which is exactly the Fagin's theorem. Using oracle machines in the polynomial hierarchy, HOji=NTIME(exp2i−2(nO(1))ΣjP)
