Page 58 - Textos de Matemática Vol. 40

46 Chapter 1. Applicative theories
statement of the axioms the expression c(f,x,n) = 0 may be read as “the computation f x converges in n steps.” The idea of these axioms is due to Friedman (unpublished) and discussed in Beeson [Bee85]. Note that these axioms are satisfied in the usual recursion-theoretic model. The constant c may be interpreted by the characteristic function of Kleene’s T predicate.
(Comp.1) ∀f, x.∀n : N.c (f, x, n) = 0 ∨ c (f, x, n) = 1, (Comp.2) ∀f,x.f x ↓ → ∃n : N.c(f,x,n) = 0.
In addition, we will restrict the universe to natural numbers. This axiom will be needed to make use of the least number operator μrec and the computabil- ity term in the definition of the least fixed point operator, see below. Of course, this axiom is absolutely in the spirit of a recursion-theoretic interpretation.
Everything is a number. Formally, this is given by the statement (AllN) ∀x.N(x).
The induction scheme for arbitrary Ll formulae is called (Ll-IN).
Now we define the applicative theory for least fixed points LFP as the union of all these axioms:
LFP := BON + (Comp) + (AllN) + (Ll-IN) .
Before we can go on and define the least fixed point operator we have to introduce some auxiliary terms. With some coding provided by pairing and projection, we can easily define a term c3 which behaves for ternary functions like c does for unary functions, i.e.,7
1. ∀f,x,y,z.∀n:N.c3(f,x,y,z,n)=0∨c3(f,x,y,z,n)=1, 2. ∀f,x,y,z.f xyz ↓ ↔ ∃n : N.c3 (f,x,y,z,n) = 0.
The following Lemma shows that there exists a function b which is never defined. Later, we will define an order relation on our functions and there b will play the role of the bottom element. Hence, we will be able the define least fixed points of monotonic functionals by recursion starting from b.
Lemma 1.8.1. There exists a closed Ll term b so that LFP proves ∀x.¬ b x ↓. Proof. From the axiom (AllN) it follows immediately that the term notN of
Corollary 1.3.2 cannot be defined. Thus, we can set b := λx.notN. ⊣
7In the presence of (AllN), the “restriction” of quantifiers to N is obviously redundant; however, it is kept here for reasons of uniformity in the expression.