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	$$classF$$
1		cI	$$classI$$
2	0 1	crdg	$$class\mathrm{rec}\left(F,I\right)$$
3		vg	$$setvarg$$
4		cvv	$$class\mathrm{V}$$
5	3	cv	$$setvarg$$
6		c0	$$class\varnothing$$
7	5 6	wceq	$$wffg=\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	$$classg\left(\bigcup \mathrm{dom}g\right)$$
14	13 0	cfv	$$classF\left(g\left(\bigcup \mathrm{dom}g\right)\right)$$
15	9 11 14	cif	$$classif\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	$$classif\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)$$