The Descriptive Complexity of the Deterministic Exponential Time Hierarchy

In Descriptive Complexity, we investigate the use of logics to characterize computational complexity classes. Since 1974, when Fagin proved that the class NP is captured by existential second-order logic, considered the first result in this area, other relations between logics and complexity classes have been established. Well-known results usually involve first-order logic and its extensions, and complexity classes in polynomial time or space. Some examples are that the first-order logic extended by the least fixed-point operator captures the class P and the second-order logic extended by the transitive closure operator captures the class PSPACE. In this paper, we will analyze the combined use of higher-order logics of order i, HOi, for i⩾2, extended by the least fixed-point operator, and we will prove that each level of this hierarchy captures each level of the deterministic exponential time hierarchy. As a corollary, we will prove that the hierarchy of HOi(LFP), for i⩾2, does not collapse, that is, HOi(LFP)⊂HOi+1(LFP)