Metamath Proof Explorer

Definition df-rdg

Description: Define a recursive definition generator on On (the class of ordinal numbers) with characteristic function F and initial value I . This combines functions F in tfr1 and G in tz7.44-1 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 (especially when df-recs that it is built on is also eliminated). But once we get past this hurdle, definitions that would otherwise be recursive become relatively simple, as in for example oav , from which we prove the recursive textbook definition as theorems oa0 , oasuc , and oalim (with the help of theorems rdg0 , rdgsuc , and rdglim2a ). We can also restrict the rec operation to define otherwise recursive functions on the natural numbers _om ; see fr0g and frsuc . 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 ) 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-seq 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 and integer powers df-exp .

Note: We introduce recwith 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. (Contributed by NM, 9-Apr-1995) (Revised by Mario Carneiro, 9-May-2015)

Ref Expression
Assertion df-rdg ${⊢}\mathrm{rec}\left({F},{I}\right)=\mathrm{recs}\left(\left({g}\in \mathrm{V}⟼if\left({g}=\varnothing ,{I},if\left(\mathrm{Lim}\mathrm{dom}{g},\bigcup \mathrm{ran}{g},{F}\left({g}\left(\bigcup \mathrm{dom}{g}\right)\right)\right)\right)\right)\right)$

Detailed syntax breakdown

Step Hyp Ref Expression
0 cF ${class}{F}$
1 cI ${class}{I}$
2 0 1 crdg ${class}\mathrm{rec}\left({F},{I}\right)$
3 vg ${setvar}{g}$
4 cvv ${class}\mathrm{V}$
5 3 cv ${setvar}{g}$
6 c0 ${class}\varnothing$
7 5 6 wceq ${wff}{g}=\varnothing$
8 5 cdm ${class}\mathrm{dom}{g}$
9 8 wlim ${wff}\mathrm{Lim}\mathrm{dom}{g}$
10 5 crn ${class}\mathrm{ran}{g}$
11 10 cuni ${class}\bigcup \mathrm{ran}{g}$
12 8 cuni ${class}\bigcup \mathrm{dom}{g}$
13 12 5 cfv ${class}{g}\left(\bigcup \mathrm{dom}{g}\right)$
14 13 0 cfv ${class}{F}\left({g}\left(\bigcup \mathrm{dom}{g}\right)\right)$
15 9 11 14 cif ${class}if\left(\mathrm{Lim}\mathrm{dom}{g},\bigcup \mathrm{ran}{g},{F}\left({g}\left(\bigcup \mathrm{dom}{g}\right)\right)\right)$
16 7 1 15 cif ${class}if\left({g}=\varnothing ,{I},if\left(\mathrm{Lim}\mathrm{dom}{g},\bigcup \mathrm{ran}{g},{F}\left({g}\left(\bigcup \mathrm{dom}{g}\right)\right)\right)\right)$
17 3 4 16 cmpt ${class}\left({g}\in \mathrm{V}⟼if\left({g}=\varnothing ,{I},if\left(\mathrm{Lim}\mathrm{dom}{g},\bigcup \mathrm{ran}{g},{F}\left({g}\left(\bigcup \mathrm{dom}{g}\right)\right)\right)\right)\right)$
18 17 crecs ${class}\mathrm{recs}\left(\left({g}\in \mathrm{V}⟼if\left({g}=\varnothing ,{I},if\left(\mathrm{Lim}\mathrm{dom}{g},\bigcup \mathrm{ran}{g},{F}\left({g}\left(\bigcup \mathrm{dom}{g}\right)\right)\right)\right)\right)\right)$
19 2 18 wceq ${wff}\mathrm{rec}\left({F},{I}\right)=\mathrm{recs}\left(\left({g}\in \mathrm{V}⟼if\left({g}=\varnothing ,{I},if\left(\mathrm{Lim}\mathrm{dom}{g},\bigcup \mathrm{ran}{g},{F}\left({g}\left(\bigcup \mathrm{dom}{g}\right)\right)\right)\right)\right)\right)$