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

Definition df-rdg 3929
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 3921 and G in tz7.44-1 3925 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 4147, from which we prove the recursive textbook definition as theorems oa0 4152, oasuc 4160, and oalim 4164 (with the help of theorems rdg0 3938, rdgsuc 3939, and rdglim 3940). We can also restrict the rec operation to define otherwise recursive functions on the natural numbers om; see fr0t 3949 and frsuct 3950. 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 operators (see df-if 2360) 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 6263 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 6898 and integer powers df-exp 6519.

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 3928 . 2 class rec(F, A)
4 vf . . . . . . . 8 set f
54cv 954 . . . . . . 7 class f
6 vx . . . . . . . 8 set x
76cv 954 . . . . . . 7 class x
85, 7wfn 3174 . . . . . 6 wff f Fn x
9 vy . . . . . . . . . 10 set y
109cv 954 . . . . . . . . 9 class y
1110, 5cfv 3179 . . . . . . . 8 class (f` y)
125, 10cres 3169 . . . . . . . . 9 class (f |` y)
13 vz . . . . . . . . . . . 12 set z
1413cv 954 . . . . . . . . . . 11 class z
15 vg . . . . . . . . . . . . . 14 set g
1615cv 954 . . . . . . . . . . . . 13 class g
17 c0 2278 . . . . . . . . . . . . 13 class (/)
1816, 17wceq 955 . . . . . . . . . . . 12 wff g = (/)
1916cdm 3167 . . . . . . . . . . . . . 14 class dom g
2019wlim 2946 . . . . . . . . . . . . 13 wff Lim dom g
2116crn 3168 . . . . . . . . . . . . . 14 class ran g
2221cuni 2500 . . . . . . . . . . . . 13 class U.ran g
2319cuni 2500 . . . . . . . . . . . . . . 15 class U.dom g
2423, 16cfv 3179 . . . . . . . . . . . . . 14 class (g` U.dom g)
2524, 1cfv 3179 . . . . . . . . . . . . 13 class (F` (g` U.dom g))
2620, 22, 25cif 2359 . . . . . . . . . . . 12 class if(Lim dom g, U.ran g, (F` (g` U.dom g)))
2718, 2, 26cif 2359 . . . . . . . . . . 11 class if(g = (/), A, if(Lim dom g, U.ran g, (F` (g` U.dom g))))
2814, 27wceq 955 . . . . . . . . . 10 wff z = if(g = (/), A, if(Lim dom g, U.ran g, (F` (g` U.dom g))))
2928, 15, 13copab 2663 . . . . . . . . 9 class {<.g, z>. | z = if(g = (/), A, if(Lim dom g, U.ran g, (F` (g` U.dom g))))}
3012, 29cfv 3179 . . . . . . . 8 class ({<.g, z>. | z = if(g = (/), A, if(Lim dom g, U.ran g, (F` (g` U.dom g))))}` (f |` y))
3111, 30wceq 955 . . . . . . 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 1644 . . . . . 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 223 . . . . 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 2945 . . . . 5 class On
3533, 6, 34wrex 1645 . . . 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 1463 . . 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 2500 . 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 955 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 3930  rdgeq1 3931  rdgeq2 3932  hbrdg 3933  rdgfnon 3936
Copyright terms: Public domain