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

Definition df-rdg 5304
 Description: Define a recursive definition generator on (the class of ordinal numbers) with characteristic function and initial value . This combines functions in tfr1 5296 and in tz7.44-1 5300 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 operation. But once we get past this hurdle, otherwise recursive definitions become relatively simple, as in for example oav 5361, from which we prove the recursive textbook definition as theorems oa0 5366, oasuc 5374, and oalim 5378 (with the help of theorems rdg0 5313, rdgsuc 5317, and rdglim2a 5322). We can also restrict the operation to define otherwise recursive functions on the natural numbers ; see fr0g 5324 and frsuc 5325. Our 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 operations (see df-if 3181) select cases based on whether the domain of is zero, a successor, or a limit ordinal. An important use of this definition is in the recursive sequence generator df-seq1 8094 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 8569 and integer powers df-exp 8196. Note: We introduce 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 multiple-part recursive definitions in the traditional textbook style.
Assertion
Ref Expression
df-rdg
Distinct variable groups:   ,,,,,   ,,,,,

Detailed syntax breakdown of Definition df-rdg
StepHypRef Expression
1 cF . . 3
2 cA . . 3
31, 2crdg 5303 . 2
4 vf . . . . . . . 8
54cv 1585 . . . . . . 7
6 vx . . . . . . . 8
76cv 1585 . . . . . . 7
85, 7wfn 4126 . . . . . 6
9 vy . . . . . . . . . 10
109cv 1585 . . . . . . . . 9
1110, 5cfv 4131 . . . . . . . 8
125, 10cres 4121 . . . . . . . . 9
13 vz . . . . . . . . . . . 12
1413cv 1585 . . . . . . . . . . 11
15 vg . . . . . . . . . . . . . 14
1615cv 1585 . . . . . . . . . . . . 13
17 c0 3082 . . . . . . . . . . . . 13
1816, 17wceq 1586 . . . . . . . . . . . 12
1916cdm 4119 . . . . . . . . . . . . . 14
2019wlim 3812 . . . . . . . . . . . . 13
2116crn 4120 . . . . . . . . . . . . . 14
2221cuni 3366 . . . . . . . . . . . . 13
2319cuni 3366 . . . . . . . . . . . . . . 15
2423, 16cfv 4131 . . . . . . . . . . . . . 14
2524, 1cfv 4131 . . . . . . . . . . . . 13
2620, 22, 25cif 3180 . . . . . . . . . . . 12
2718, 2, 26cif 3180 . . . . . . . . . . 11
2814, 27wceq 1586 . . . . . . . . . 10
2928, 15, 13copab 3565 . . . . . . . . 9
3012, 29cfv 4131 . . . . . . . 8
3111, 30wceq 1586 . . . . . . 7
3231, 9, 7wral 2355 . . . . . 6
338, 32wa 337 . . . . 5
34 con0 3811 . . . . 5
3533, 6, 34wrex 2356 . . . 4
3635, 4cab 2128 . . 3
3736cuni 3366 . 2
383, 37wceq 1586 1
 Colors of variables: wff set class This definition is referenced by:  dfrdg2 5305  rdgeq1 5306  rdgeq2 5307  hbrdg 5308  rdgfnon 5311