HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Definition df-rdg 4231
Description: Define a recursive definition generator on On (the class of ordinal numbers) with characteristic function F and initial value A. This combines functions F in tfr1 4223 and G in tz7.44-1 4227 into one definition. This rather amazing operation allows us to define, with compact direct definitions, functions that are usually defined in textbooks only with indirect self-referencing recursive definitions. A recursive definition requires advanced metalogic to justify - in particular, eliminating a recursive definition is very difficult and often not even shown in textbooks. On the other hand, the elimination of a direct definition is a matter of simple mechanical substitution. The price paid is the daunting complexity of our rec operation. But once we get past this hurdle, otherwise recursive definitions become relatively simple, as in for example oav 4284, from which we prove the recursive textbook definition as theorems oa0 4289, oasuc 4297, and oalim 4301 (with the help of theorems rdg0 4240, rdgsuc 4244, and rdglimi 4242). We can also restrict the rec operation to define otherwise recursive functions on the natural numbers om; see fr0g 4251 and frsuc 4252. Our rec operation apparently does not appear in published literature, although closely related is Definition 25.2 of [Quine] p. 177, which he uses to "turn...a recursion into a genuine or direct definition" (p. 174). Note that the if operations (see df-if 2415) select cases based on whether the domain of g is zero, a successor, or a limit ordinal.

An important use of this definition is in the recursive sequence generator df-seq1 6671 on the natural numbers (as a subset of the complex numbers), allowing us to define, with direct definitions, recursive infinite sequences such as the factorial function df-fac 7133 and integer powers df-exp 6762.

Note: We introduce rec with the philosophical goal of being able to eliminate all definitions with direct mechanical substitution and to verify easily the soundness of definitions. Metamath itself has no built-in technical limitation that prevents recursive definitions in the traditional textbook style.

Assertion
Ref Expression
df-rdg |- rec(F, A) = U.{f | E.x e. On (f Fn x /\ A.y e. x (f` y) = ({<.g, z>. | z = if(g = (/), A, if(Lim dom g, U.ran g, (F` (g` U.dom g))))}` (f |` y)))}
Distinct variable groups:   x,y,z,f,g,F   x,A,y,z,f,g

Detailed syntax breakdown of Definition df-rdg
StepHypRef Expression
1 cF . . 3 class F
2 cA . . 3 class A
31, 2crdg 4230 . 2 class rec(F, A)
4 vf . . . . . . . 8 set f
54cv 990 . . . . . . 7 class f
6 vx . . . . . . . 8 set x
76cv 990 . . . . . . 7 class x
85, 7wfn 3257 . . . . . 6 wff f Fn x
9 vy . . . . . . . . . 10 set y
109cv 990 . . . . . . . . 9 class y
1110, 5cfv 3262 . . . . . . . 8 class (f` y)
125, 10cres 3252 . . . . . . . . 9 class (f |` y)
13 vz . . . . . . . . . . . 12 set z
1413cv 990 . . . . . . . . . . 11 class z
15 vg . . . . . . . . . . . . . 14 set g
1615cv 990 . . . . . . . . . . . . 13 class g
17 c0 2331 . . . . . . . . . . . . 13 class (/)
1816, 17wceq 991 . . . . . . . . . . . 12 wff g = (/)
1916cdm 3250 . . . . . . . . . . . . . 14 class dom g
2019wlim 2975 . . . . . . . . . . . . 13 wff Lim dom g
2116crn 3251 . . . . . . . . . . . . . 14 class ran g
2221cuni 2568 . . . . . . . . . . . . 13 class U.ran g
2319cuni 2568 . . . . . . . . . . . . . . 15 class U.dom g
2423, 16cfv 3262 . . . . . . . . . . . . . 14 class (g` U.dom g)
2524, 1cfv 3262 . . . . . . . . . . . . 13 class (F` (g` U.dom g))
2620, 22, 25cif 2414 . . . . . . . . . . . 12 class if(Lim dom g, U.ran g, (F` (g` U.dom g)))
2718, 2, 26cif 2414 . . . . . . . . . . 11 class if(g = (/), A, if(Lim dom g, U.ran g, (F` (g` U.dom g))))
2814, 27wceq 991 . . . . . . . . . 10 wff z = if(g = (/), A, if(Lim dom g, U.ran g, (F` (g` U.dom g))))
2928, 15, 13copab 2739 . . . . . . . . 9 class {<.g, z>. | z = if(g = (/), A, if(Lim dom g, U.ran g, (F` (g` U.dom g))))}
3012, 29cfv 3262 . . . . . . . 8 class ({<.g, z>. | z = if(g = (/), A, if(Lim dom g, U.ran g, (F` (g` U.dom g))))}` (f |` y))
3111, 30wceq 991 . . . . . . 7 wff (f` y) = ({<.g, z>. | z = if(g = (/), A, if(Lim dom g, U.ran g, (F` (g` U.dom g))))}` (f |` y))
3231, 9, 7wral 1690 . . . . . 6 wff A.y e. x (f` y) = ({<.g, z>. | z = if(g = (/), A, if(Lim dom g, U.ran g, (F` (g` U.dom g))))}` (f |` y))
338, 32wa 221 . . . . 5 wff (f Fn x /\ A.y e. x (f` y) = ({<.g, z>. | z = if(g = (/), A, if(Lim dom g, U.ran g, (F` (g` U.dom g))))}` (f |` y)))
34 con0 2974 . . . . 5 class On
3533, 6, 34wrex 1691 . . . 4 wff E.x e. On (f Fn x /\ A.y e. x (f` y) = ({<.g, z>. | z = if(g = (/), A, if(Lim dom g, U.ran g, (F` (g` U.dom g))))}` (f |` y)))
3635, 4cab 1504 . . 3 class {f | E.x e. On (f Fn x /\ A.y e. x (f` y) = ({<.g, z>. | z = if(g = (/), A, if(Lim dom g, U.ran g, (F` (g` U.dom g))))}` (f |` y)))}
3736cuni 2568 . 2 class U.{f | E.x e. On (f Fn x /\ A.y e. x (f` y) = ({<.g, z>. | z = if(g = (/), A, if(Lim dom g, U.ran g, (F` (g` U.dom g))))}` (f |` y)))}
383, 37wceq 991 1 wff rec(F, A) = U.{f | E.x e. On (f Fn x /\ A.y e. x (f` y) = ({<.g, z>. | z = if(g = (/), A, if(Lim dom g, U.ran g, (F` (g` U.dom g))))}` (f |` y)))}
Colors of variables: wff set class
This definition is referenced by:  dfrdg2 4232  rdgeq1 4233  rdgeq2 4234  hbrdg 4235  rdgfnon 4238
Copyright terms: Public domain