skip to content

Complete problems for higher order logics

Wednesday 15th February 2006 - 11:30 to 12:30
INI Seminar Room 1

Let $i, j \geq 1$, and let $\Sigma^i_j$ denote the class of the higher order logic formulas of order $i+1$ with $j-1$ alternations of quantifier blocks of variables of order $i+1$, starting with an existential quantifier block. There is a precise correspondence between the non deterministic exponential time hierarchy and the different fragments of higher order logics $\Sigma^i_j$, namely $NEXP^j_i= \Sigma^{i+1}_j$.

In this article we present a complete problem for each level of the non deterministic exponential time hierarchy, with a very weak sort of reductions, namely quantifier-free first order reductions. Moreover, we don't assume the existence of an order in the input structures in this reduction. From the logical point of view, our main result says that every fragment $\Sigma^i_j$ of higher order logics can be captured with a first order logic Lindstrom quantifier. Moreover, as our reductions are quantifier-free first order formulas, we get a normal form stating that each $\Sigma^i_j$ sentence is equivalent to a single occurrence of the quantifier and a tuple of quantifier-free first order formulas.

Our complete problems are a generalization of the well known problem quantified Boolean formulas with bounded alternation.

University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons