Finite model theory for partially ordered connectives
Merlijn Sevenster, Tero Tulenheimo

Abstract:
In the present article a study of the finite model theory of Henkin
quantifiers with boolean variables, a.k.a. partially ordered
connectives, is undertaken. The logic of first-order formulae prefixed
by partially ordered connectives, denoted D, is considered on finite
structures. D is characterized as a fragment of second-order
existential logic \Sigma^1_1; the formulae of the relevant fragment do
not allow existentially quantified variables as arguments of predicate
variables.  Using this characterization result, D is shown to harbor a
strict hierarchy induced by the arity of predicate variables. Further,
D is shown to capture NP over linearly ordered structures, and not to
be closed under complementation. We conclude with a comparison between
the logics D and \Sigma^1_1 on several metatheoretical properties.