S. Kuznetsov. *-continuity vs. induction: divide and conquer
Abstract
The Kleene star can be axiomatised in two ways: inductively, as a fixpoint, or as
the ω-iteration of multiplications. The latter is called *-continuity and is stronger
than the former: not every Kleene algebra is *-continuous. In the language of only
multiplication, union, and Kleene star, however, the (in)equational atomic theory
(logic) of *-continuous Kleene algebras coincides with the one of all Kleene algebras
(Kozen, 1994). The situation changes dramatically when one adds division operations.
As shown by Buszkowski (2007), then the logic with *-continuity becomes \(\Pi_1^0\)-hard
and therefore strictly stronger than the inductive one. This result, however, is not
constructive, i.e., does not yield a formula distingushing them.
Our contribution is threefold. First, we present an example of Kleene algebra with
divisions and intersection, which is not *-continuous. Second, we present a formula
which makes Buszkowski’s result constructive (see above). Third, we show that the
calculus for *-continuity is incomplete w.r.t. more specific relational and language
models, in the fragment with divisions, multiplication, intersection, and Kleene star.
The choice of this fragment is natural, since union or the unit constant are known to
yield incompleteness even without Kleene star.