caa a22 4500 463187148 CHVBK 20180406164857.0 cr unu---uuuuu 170326e20070601xx s 000 0 eng 10.1007/s10472-007-9071-4 doi (NATIONALLICENCE)springer-10.1007/s10472-007-9071-4 Arity and alternation: a proper hierarchy in higher order logics [Elektronische Daten] [Flavio Ferrarotti, José Turull Torres] We study the effect of simultaneously bounding the maximal-arity of the higher-order variables and the alternation of quantifiers in higher-order logics, as to their expressive power on finite structures (or relational databases). Let $\mathit{AA}^i(r,m)$ be the class of (i + 1)-th order logic formulae where all quantifiers are grouped together at the beginning of the formulae, forming m alternating blocks of consecutive existential and universal quantifiers, and such that the maximal-arity (a generalization of the concept of arity, not just the maximal of the arities of the quantified variables) of the higher-order variables is bounded by r. Note that, the order of the quantifiers in the prefix may be mixed. We show that, for every i ≥ 1, the resulting $\mathit{AA}^i(r,m)$ hierarchy of formulae of (i + 1)-th order logic is proper. This extends a result by Makowsky and Pnueli who proved that the same hierarchy in second-order logic is proper. In both cases the strategy used to prove the results consists in considering formulae which, represented as finite structures, satisfy themselves. As the well known diagonalization argument applies here, this gives rise, for each order i and each level of the $\mathit{AA}^i(r,m)$ hierarchy of arity and alternation, to a class of formulae which is not definable in that level, but which is definable in a higher level of the same hierarchy. We then use a similar argument to prove that the classes of $\Sigma^i_m \cup \Pi^i_m$ formulae in which the higher-order variables of all orders up to i + 1 have maximal-arity at most r, also induce a proper hierarchy in each higher-order logic of order i ≥ 3. It is not known whether the correspondent hierarchy in second-order logic is proper. Using the concept of finite model truth definitions introduced by M. Mostowski, we give a sufficient condition for that to be the case. Springer Science+Business Media B.V., 2007 Expressibility nationallicence Higher-order logics nationallicence Quantifier alternation nationallicence Quantifier arity nationallicence Ferrarotti Flavio Information Science Research Centre, Department of Information Systems, Massey University, P.O. Box 756, Wellington, New Zealand aut Turull Torres José Information Science Research Centre, Department of Information Systems, Massey University, P.O. Box 756, Wellington, New Zealand aut Annals of Mathematics and Artificial Intelligence Springer Netherlands 50/1-2(2007-06-01), 111-141 1012-2443 50:1-2<111 2007 50 10472 https://doi.org/10.1007/s10472-007-9071-4 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/s10472-007-9071-4 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Ferrarotti Flavio Information Science Research Centre, Department of Information Systems, Massey University, P.O. Box 756, Wellington, New Zealand aut NATIONALLICENCE 700 1- Turull Torres José Information Science Research Centre, Department of Information Systems, Massey University, P.O. Box 756, Wellington, New Zealand aut NATIONALLICENCE 773 0- Annals of Mathematics and Artificial Intelligence Springer Netherlands 50/1-2(2007-06-01), 111-141 1012-2443 50:1-2<111 2007 50 10472 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer