In this chapter we show how an appropriate first-order language can be built up to describe the properties of rP σ 1 -programs. Here we also use the logical tools introduced in Chapter 13, and the method of the development of the required dynamic logics is similar to that used in the previous chapter. We have proved in Part I that rP σ 1 ≈I for a one-sorted similarity type σ. Thus first we present a logic within which any fixed-point equation of the form R(X) ≡ φ(X, P) (φ ∈ Σ+(σ,R)) has a solution. Secondly, we show how the semantics of rP σ 1 can be defined, and using this definition we give an appropriate semantic function \( \hat \cdot :rD_\sigma ^1 \to Form_\delta \). Finally we give similar characterizations and completeness results to those in Chapter 14.