Page 48 - Textos de Matemática Vol. 40

36
Chapter 1. Applicative theories
1. tF is k-N-strict (in T ), and
2. tF provably represents F (in T ), i.e.,
(a) for all m1,...,mk,n ∈ IN,
F(m1,...,mk)=n⇔T ⊢tF m1 ...mk =n,
(b) T ⊢(tF :Nk →N).
To prove that all provably representable function are also strongly repre- sentable in the presence of (N-Str) we define a term ifN. This term allows to check whether an argument of a function belongs to N.
Lemma 1.7.15. There exists a term ifN of Lp such that
BON + (N-Str) ⊢ (N(ifN x y) → N(x)) ∧ (N(x) → ifN x y = y).
Proof. DefineifN :=λx,y.dNy0xx. ⊣ Using ifN for each argument of a k-ary function the following Proposition
is easy to verify:
Proposition 1.7.16. If tF provably represents F : INk → IN in the theory T
(which is an extension of BON) then
λx1....λxk.ifN x1 (...(ifN xk (tF x1 ... xk))···)
strongly represents F in T + (N-Str).
This result yields another proof of both Lemma 1.7.8 and 1.7.10 if we choose sdN and andN as strong representations of the constant-zero function and an arbitrary primitive-recursive, binary function.
Remark 1.7.17. To leave the meaning of dN untouched we may introduce N- strictness by adding ifN as a new constant to Lp and taking the formula of Lemma 1.7.15 as additional axiom instead of adding (N-Str). Then a term d′N which satisfies the axioms of dN and (N-Str) is easily definable by d′N := λu,v,x,y.ifN x(ifN y(dN uvxy)).
Another example of an application of (N-Str) is the possibility to establish a one-one relation between total functions and sets. That means, we can define a term set such that
BON + (N-Str) ⊢
∀f.((f :N→N)↔setf ∈P(N))∧∀x:N.(fx=0↔(setf)=0).
For set we can choose λf, x.dN 0 1 (f x) 0. Note that we cannot prove the direc- tions from the right to the left in the conjunctions without (N-Str).