An essay in combinatory dynamic logic

choice function Combinatory Propositional Dynamic Logic completeness decidability extensions of CPDL finitary axiomatization finite model property quantification soundness Stone representation theorem for combinatory dynamic algebras

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70)

Review text

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.

Recommendations

Cites work

Cited in

(50)

This page was built for publication: An essay in combinatory dynamic logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q809068)