A Mu-Calculus

Abstract

The logical framework presented in the previous chapter is an axiomatization of the entailment on assertions using terms, types, and meta-predicates. These assertions were interpreted as compact open sets of the domains associated with the types. The expressive power of the logic is, therefore, not as strong as one sometimes would like. There is no assertion, for example, of the type of natural numbers to express ‘the set of even numbers’. To make the logic more expressive some extra structure on assertions is needed. One of the possible ways to get a richer assertion language is to introduce fixed-point operators.