Page 67 - Textos de Matemática Vol. 40

1.8. A case study: least fixed points 55
the universal class x = x and ∅ the empty class x ̸= x. Then the functional λf,x.f x is an element of (V∅) → (V∅) and is of course V∅ monotonic. Therefore, by Lemma 1.8.10 we have l (λf, x.f x) ∈ (V ∅) and this implies ∀y.¬ l (λf, x.f x) y ↓. Hence we have proven in LFP that the method m loops forever.
It is easy to observe that LFP can be interpreted in the usual recursion theoretic model. In fact, the computability axioms are inspired by Kleene’s T predicate, which therefore may be used to verify the axioms. So we can reduce LFP to Peano arithmetic. In fact, Studer used this fact to obtain expressively strong but proof-theoretically weak systems for the study of object-oriented programming languages, cf. [Stu01a, Stu01b].
The investigation of a least fixed point operator in [Kah92] was motivated by defining an applicative theory with proof-theoretic strength of Peano arith- metic for studying the interactive proof system lambda [FF90, FFM90]. This proof system was designed for proving properties of ml programs. Up to Release 3.2 it was based on a partial logic and it was generating minimality rules for recursive function definitions. The theory defined in [Kah92] was capturing a large part of this proof system, in particular, the minimality rules were modeled using the least fixed point operator.
Finally let us address two related approaches. First, Feferman [Fef92] develops a form of generalized recursion theory in which computational proce- dures on domains that are contained in the natural numbers reduce to ordinary computations. There he shows how to obtain a uniform index for the least fixed point operator in the intensional recursion-theoretic model of computation. In fact, the construction of our least fixed point combinator is inspired by this approach.
Secondly, Sta¨rk [St¨a98, St¨a05] introduces a typed logic of partial terms, based on BPT, cf. Section 1.1.3, which incorporates a least fixed point operator and a schema for computational induction. One may ask why we do not axiom- atize our fixed point operator in a similar way as a primitive operator instead of using the computability axioms. The reason is that formulating Theorem 1.8.12 as an axiom would require to introduce beforehand the notions of monotonicity and classes. In our opinion, this would be a rather inelegant approach since the axioms would already depend on complex, abbreviated notions.