No label defined (Q4029612)

[For the entire collection see Zbl 0745.00057.] In this paper we introduce a generalization of PDL and dynamic algebras in which the operation of iteration procedure \(\alpha^*\) is replaced by a more complex recursion operator on programs \(\Gamma_ \omega(\alpha_ 1,\dots,\alpha_ n)\). An arithmetical axiomatization of a first-order dynamic logic with recursive procedures is given by \textit{D. Harel} [First-order dynamic logic (Lect. Notes Comput. Sci. 68) (1979; Zbl 0403.03024)] (Harel calls his logic a context-free dynamic logic --- CFDL). In this paper we consider a kind of a propositional version of CFDL and give for it an infinitary axiomatization in the style of \textit{G. Mirkowska} [Lect. Notes Comput. Sci. 125, 23-101 (1981; Zbl 0487.03012)] and \textit{R. Goldblatt} [Axiomatising the logic of computer programming (Lect. Notes Comput. Sci. 130) (1982; Zbl 0474.68045)] and a completeness theorem with respect to a fixed-point semantics. For that purpose we first introduce the notion of \(\Gamma_ \omega\)-dynamic algebra and give an analog of the Stone set- representation theorem for some class of such algebras.