Dynamic Logic Generated by Extension

Abstract

As we have seen, the σ-type dynamic logic and even its Floyd-Hoare sublanguage are incomplete. The efforts made in the previous chapter to make dynamic logic complete did not bring us pragmatically satisfactory results. Therefore, we now look for another way to obtain a pragmatically satisfactory complete dynamic logic. First of all we require that this way should allow us to preserve the classical notion of completeness and should also provide us with the expected dynamic logic in the scope of classical first-order logic. The latter requirement follows from our original aim to develop programming theory in this scope. Moreover, we also require to develop the dynamic logic in compliance with the computation theory developed in Part 1. In the present chapter we introduce the main logical tools which can be used to develop different programming logic as classical first-order languages. These tools are based on the notion of extension introduced in Chapter 5 and are used to augment the programming language r P ^σ with different computational devices.