Dot-Depth and Monadic Quantifier Alternation over Pictures
Oliver Matz
In formulas of monadic second-order logic (MSO), quantifiers
range over set of elements or over elements of the universe
of some finite structure.
Fagin has shown in 1974 that not every MSO-formula is
equivalent to an existential one, i.e., a formula with a set
quantifier prefix of existential set quantifiers only, followed
by a first-order kernel formula (i.e. without set quantifiers).
Fagin asked in 1995 whether in MSO-formulas the quantifier
alternation depth of ``exist''-quantifiers on one hand and
``for-all''-quantifiers on the other hand can be bounded; in
other words, whether there is a k>1 such that every MSO-formula
is equivalent to one with a set quantifier prefix of k blocks
of set quantifiers, existential and universal in alternation,
followed by a first-order kernel formula.
The thesis shows that this is not the case, even for a
particular class of finite structure, the so-called ``grids''.
Moreover, we investigate to what extent the alternation of
first-order quantifiers is responsible for the increase of
expressive power.
The investigation of these questions yields as a
by-product results about ``picture languages'', which are
the two-dimensional analogue to classical (one-dimensional)
languages. In particular it is shown that there is a starfree,
non-recognizable picture language, although both the notion
of ``starfreeness'' and that of ``recognizability'' are
straightforward generalizations of the corresponding notions
is the setting of classical languages.