Page 49 - Textos de Matemática Vol. 40

1.7. N-strictness 37 1.7.3 Quantification operators
In the following we discuss the logical relationship of the three quantification operators μ, E0, and E#0 , introduced in Section 1.6. It turns out that some properties of these operators are closely related to the question of N-strictness.
The following investigation will make clear, that only E0 is definable from μ over BON. To get μ from E0 we need N-strictness as well as formulae induction. Nevertheless, we can show that andN and sdN are definable in BON(E0) without using N-strictness. So we get the equivalence of (O-IN) and (N-IN) in BON(E0) and BON(μ).
Because E#0 operates on partial functions we cannot expect that it is de- finable by E0 or μ. But for the converse we will need N-strictness to get the totality test for functions contained in the first axiom of E0 and μ.
Proposition 1.7.18. There exists a term E0μ of Lμ such that
1. BON(μ)⊢(f :N→N)↔N(E0μf),
2. BON(μ)⊢(f :N→N)→((∃x:N.fx=0)↔E0μf =0).
Proof. We define E0μ :=
λf.μ(λx.dN (f (μf))
(dN (dN 10(f (μf))0)
(μ(λy.dN 1(dN 0(μf)y1)y0))
x1) x 0).
More readable E0μ may be written as λf.μ (λx.g f x) with
and
μ(λy.hf y),  1,
if x > 1,
if y = 0,
 f(μf), ifx=0, gfx:= dN10(f(μf))0, ifx=1,
hfy:= 0,
The idea of the construction of E0μ is to define a new function g f associated
with f in such a way that
1. gf is total, if and only if f is total, 2. assuming f is total, then
(a) gf has exactly one zero at 0, if and only if f has a zero, (b) gf hasazero,butnotat0,ifandonlyiff hasnozero.
ify=1, μf, ify>1.