Page 59 - Textos de Matemática Vol. 40

1.8. A case study: least fixed points 47 1.8.2 Least fixed point operator
In this Section we will show how to define a least fixed point operator l in the theory LFP. As usual, in order to find the least fixed point of a monotonic functional g, the operator l will iterate g starting from the bottom element b. The stages of this inductive process are given by the term h, which will be defined first.
Definition 1.8.2. We define the term h so that
b
g (h g (pN n))
if n = 0, otherwise.
hgn≃ Let q be such that

qgxn≃
Then the term l is defined by
l := λg, x.p1 (p0 (μrec (λy.c3 (q, g, x, p0 y, p1 y)))).
The idea of this definition can be explained roughly as follows. We would like to have that lgx = z implies that there exists a finite computation of z by iterating the operator g starting from b. Formally, this is expressed by ∃n.h g n x = z, cf. the third Claim of the following Lemma. The definition of l is somewhat clumsy because of the several codings. Let g and x be given, then the μrec operator is looking for an n so that
c3 (q,g,x,p0 n,p1 n) = 0. (10)
If there is no such natural number n, then μrec(λy.c3 (q, g, x, p0 y, p1 y)) will be undefined. Assume we have found an n so that (10) holds. This means that q g x (p0 n) is terminating in p1 n steps. By the definition of q, we obtain that q g x (p0 n) ↓ implies h g (p0 (p0 n)) x = p1 (p0 n). Finally, the outer projections are used to extract this value p1 (p0 n).
The behavior of l may be also gathered from (the proof of) the following Lemma. Moreover, it also shows why we had to include the axiom (AllN) to LFP. Without this axiom the sophisticated interplay between the least number operator μrec, the computability term c3, and the coding machinery provided by p0,p1 and p would hardly work. This proof also makes use of the fact that the projection functions are total, see axiom II.(3) of BON.
Lemma 1.8.3. LFP proves: 1. lg↓,
2. lgx ↓ ↔ ∃n.hgnx ↓,
3. lgx=z→∃n.hgnx=z.
0 if h g (p0 n) x = p1 n, notN otherwise.