Page 57 - Textos de Matemática Vol. 40

1.8. A case study: least fixed points 45
With respect to this ordering relation, we can talk about leastness of fixed points. Since not every recursion equation has a least fixed point, we additionally need the notion of monotonicity which can be given using the definedness ordering. Moreover, we will introduce the concept of classes, which are similar to types in a typed setting, in order to prove that our least fixed point belongs to a certain function space.
Since in general there are total term models for applicative theories we often cannot prove that there exist undefined terms or equivalently that the corresponding programs loop forever. For this reason we strengthen the basic theory by so-called computability axioms and we restrict the universe to natural numbers. These additional axioms represent the recursion-theoretic view of computations. They are motivated by Kleene’s T predicate which is a ternary primitive recursive relation on the natural numbers so that {a}(m⃗ ) ≃ n holds if and only if there exists a computation sequence u with T(a, ⟨m⃗ ⟩, u) and (u)0 = n. The use of these computability axioms for the definition of a least fixed point operator may be seen as a marriage of convenience of the recursion-theoretic semantics and the least fixed point semantics for computer programs, cf. e.g., Jones [Jon97].
Using the computability axioms we will define the least fixed point combi- nator as a combinator iterating the functional operator associated with a given recursive equation starting from the totally undefined function. To get the de- sired properties we have to ensure that the functional operator is monotone with respect to the definedness order. For this reason we will need the notion of monotonicity mentioned above.
The given theory still has a standard recursion-theoretic model; and with respect to the proof-theoretic strength we will not exceed Peano arithmetic.
There exists a standard theory to formalize least fixed points, namely the theory ID1 of non-iterated positive arithmetical inductive definitions, cf. e.g., Moschovakis [Mos74] for an introduction to inductive definability or the Section 2.2.1 for a corresponding theory in the context of explicit mathemat- ics. However, our work essentially concerns Σ01 monotone inductive definitions whereas ID1 deals with arbitrary arithmetically definable positive operators. Hence ID1 belongs to a rather different “world” and with respect to its proof- theoretic strength it is much stronger than Peano arithmetic.
1.8.1 The theory LFP
The language Ll is the language Lp of BON extended by one new constant:
• c (computation).
We are interested in the extension of BON with axioms about computability (Comp) and the assertion that everything is a number.
Computability. These axioms are intended to capture the idea that con- vergent computations should converge in finitely many steps. In the formal