Expressibility of Higher Order Logics
Lauri Hella, José María Turull-Torres · Electronic Notes in Theoretical Computer Science · 2003
We study the expressive power of higher order logics on finite relational structures or databases. First, we give a characterization of the expressive power of the fragments Σij and πij, for each order i ≥ 2 and each number of alternations of quantifier blocks j. Then we get as a corollary the expressive power of HOi for each order i ≥ 2. From our results, as well as from the results of D. Leivant and of R. Hull and J. Su, it turns out that no higher order logic can be complete. Even if we consider the union of higher order logics of all natural orders, i.e., Ui≥2 HOi, we still do not get a complete logic. So, we define a logic which we call variable order logic (VO) which permits the use of untyped relation variables, i.e., variables of variable order, by allowing quantification over orders. We show that this logic is complete.