Fixed Points

Abstract

The primary significance of the Recursion Theorem 5.6 is foundational, since the result justifies on the basis of the axioms a method of definition of functions which is intuitively obvious. From a purely mathematical point of view, however, we can also view 5.6 as a theorem of existence and uniqueness of solutions for systems of identities of the form

$$f(0) = a,\,\,\,f(Sx) = h(f(x))\,\,\,\,\,\,\,(x \in N)$$

((6.1))

where a ∈ E and h : E → E are given and the function f : N → E is the unknown. In this chapter we will prove an elegant generalization of the Recursion Theorem in the context of the theory of partial orderings, which implies the existence and uniqueness of solutions for systems of functional identities much more general than (6.1). The Continuous Least Fixed Point Theorem 6.21 is fundamental for the theory of computation, it is the basic mathematical tool of the so-called fixpoint theory of programs. In the next chapter we will show that it is a special case of a much deeper Fixed Point Theorem of Zermelo, which is intimately related to the theory of wellorderings and rich in set theoretic consequences, for example it implies directly the Hypothesis of Cardinal Comparability, 3.1. Thus, in addition to its purely mathematical significance, the Continuous Least Fixed Point Theorem yields also an interesting point of contact between classical set theory and today’s theoretical computer science.