zbMATH — the first resource for mathematics

The alternation hierarchy for the theory of \(\mu\)-lattices. (English) Zbl 0987.03057
Summary: The alternation hierarchy problem asks whether every \(\mu\)-term \(\phi\), that is, a term built up also using a least fixed point constructor as well as a greatest fixed point constructor, is equivalent to a \(\mu\)-term where the number of nested fixed points of a different type is bounded by a constant independent of \(\phi\). In this paper we give a proof that the alternation hierarchy for the theory of \(\mu\)-lattices is strict, meaning that such a constant does not exist if \(\mu\)-terms are built up from the basic lattice operations and are interpreted as expected. The proof relies on the explicit characterization of free \(\mu\)-lattices by means of games and strategies.

03G30 Categorical logic, topoi
06B25 Free lattices, projective lattices, word problems
68Q60 Specification and verification (program logics, model checking, etc.)
91A43 Games involving graphs
03B70 Logic in computer science
03C05 Equational classes, universal algebra in model theory
Full Text: EMIS EuDML