×

*-continuity vs. induction: divide and conquer. (English) Zbl 1418.03111

Bezhanishvili, Guram (ed.) et al., Advances in modal logic. Vol. 12. Proceedings of the 12th conference (AiML 2018), Bern, Switzerland, August 27–31, 2018. London: College Publications. 493-510 (2018).
Summary: The Kleene star can be axiomatised in two ways: inductively, as a fixpoint, or as the \(\omega\)-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 ([D. Kozen, Inf. Comput. 110, No. 2, 366–390 (1994; Zbl 0806.68082)]). The situation changes dramatically when one adds division operations. As shown by W. Buszkowski [J. Log. Comput. 17, No. 1, 199–217 (2007; Zbl 1118.03013)], 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.
For the entire collection see [Zbl 1398.03005].

MSC:

03B47 Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics)
03G25 Other algebras related to logic
68Q45 Formal languages and automata
PDFBibTeX XMLCite