Skip to content

LAA

Seminar

Complete problems for higher order logics

Hella, L (Tampere)
Wednesday 15 February 2006, 11:30-12:30

Seminar Room 1, Newton Institute

Abstract

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.

Back to top ∧