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 rec F I = recs g V if g = I if Lim dom g ran g F g dom g

Detailed syntax breakdown

Step Hyp Ref Expression
0 cF class F
1 cI class I
2 0 1 crdg class rec F I
3 vg setvar g
4 cvv class V
5 3 cv setvar g
6 c0 class
7 5 6 wceq wff g =
8 5 cdm class dom g
9 8 wlim wff Lim dom g
10 5 crn class ran g
11 10 cuni class ran g
12 8 cuni class dom g
13 12 5 cfv class g dom g
14 13 0 cfv class F g dom g
15 9 11 14 cif class if Lim dom g ran g F g dom g
16 7 1 15 cif class if g = I if Lim dom g ran g F g dom g
17 3 4 16 cmpt class g V if g = I if Lim dom g ran g F g dom g
18 17 crecs class recs g V if g = I if Lim dom g ran g F g dom g
19 2 18 wceq wff rec F I = recs g V if g = I if Lim dom g ran g F g dom g