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
ϕ
=
∃
X
1
i
¯
∀
X
2
i
¯
…
Q
X
j
i
¯
ψ
where
Q
is a quantifier,
Q
X
i
¯
means that
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
∃
, 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
…
2
x
with
i
times
2
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.
HO is equal to ELEMENTARY functions. To be more precise,
H
O
0
i
=
N
T
I
M
E
(
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
∃
S
O
=
H
O
0
2
=
N
T
I
M
E
(
n
O
(
1
)
)
=
N
P
, which is exactly the Fagin's theorem. Using oracle machines in the polynomial hierarchy,
H
O
j
i
=
N
T
I
M
E
(
exp
2
i
−
2
(
n
O
(
1
)
)
Σ
j
P
)
