An essay in combinatory dynamic logic (Q809068): Difference between revisions

The present extensive paper analyses Combinatory Propositional Dynamic Logic (CPDL) as a fusion of two ideas in the authors' Ph. D. theses: names in modal logic (S. Passy, 1984), and \(\omega\)-axiomatics in dynamic logic (T. Tinchev, 1986). The CPDL language is defined as follows: let \(\Sigma\), \(\Phi_ 0\) and \(\Pi_ 0\) be three countably infinite and pairwise disjoint alphabets, labelled, respectively, as names (or constants), atomic propositions, and atomic programs. The letter \(\nu \not\in \Sigma \cup \Phi_ 0\cup \Pi_ 0\) is called the universe program (or modality). The language of CPDL consists of formulae and programs, inductively defined by: (i) The elements of \(\Sigma \cup \Phi_ 0\) are formulae. The elements of \(\Pi_ 0\cup \{\nu \}\) are programs; (ii) If A, B are formulae, and \(\alpha\), \(\beta\) are programs, then: \(\neg A\), \(A\vee B\), \(<\alpha >A\) are formulae, and \(\alpha\) ;\(\beta\), \(\alpha\cup \beta\), \(\alpha^*\), A? are programs. For \(CPDL^{\cap}\) there is added the clause ``\(\alpha\cap \beta\) is a program''. After an explanatory Prologue, discussing the reasons and purposes of the paper, Chapter 1 gives a fairly detailed approach to CPDL, easily extendable to \(CPDL^{\cap}\). Sections 1-6 contain: the relation to Scott's isomorphism theorem, CPDL axiomatization and proof theory, soundness and completeness for simple extensions of CPDL and \(CPDL^{\cap}\), finitary axiomatization, the finite model property and hence decidability for CPDL. Chapter 2 discusses some interesting extensions of CPDL: Section 2 is motivated by some definitional extensions which are traditionally in the scope of dynamic and modal logics. Section 3 deals with some extensions treating infinity. In Section 4, two exotic extensions of CPDL, admitting a choice function in the models, are proposed. Section 5 discusses CPDL extensions towards polyadic and multi-ary CPDL theory. In Section 6 the authors prove results on the high undecidability of an important number of CPDL extensions, listing open questions concerning the decidability of \(CPDL^{\cap}\) and some of its extensions, and discussing the rôle of the \(\omega\)-rule for finitary incompleteness. Finally, Chapter 3 is devoted to quantification in CPDL (CDL). The CDL language extends the CPDL syntax by: \(\exists cA\) is a formula, and \(\forall cA=\neg \exists c\neg A\). Denoting by [d/c]A the formula obtained by substituting c with d (if possible), then the semantics of CDL is: \(s\vDash \exists cA\) iff \(s\vDash [d/c]A\), for some \(d\in \Sigma\). The authors prove the completeness of CDL, discuss axiomatization through expressiveness, and give results on undecidability and finitary incompleteness of CDL. The Appendix contains a Stone representation theorem for combinatory dynamic algebras. This substantial paper points out many interesting results, relations and insights within the context of dynamic logics, including useful comments, evolutions, trends, and schools (particularly the Bulgarian one) in the field.