The INI has a new website!

This is a legacy webpage. Please visit the new site to ensure you are seeing up to date information.

An Isaac Newton Institute Programme

Logic and Algorithms

Complete problems for higher order logics

13th February 2006

Authors: Lauri Hella (University of Tampere), Jose Maria Turull-Torres (Massey University)


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.

Related Links