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 e. _V |-> if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cF | |- F |
|
| 1 | cI | |- I |
|
| 2 | 0 1 | crdg | |- rec ( F , I ) |
| 3 | vg | |- g |
|
| 4 | cvv | |- _V |
|
| 5 | 3 | cv | |- g |
| 6 | c0 | |- (/) |
|
| 7 | 5 6 | wceq | |- g = (/) |
| 8 | 5 | cdm | |- dom g |
| 9 | 8 | wlim | |- Lim dom g |
| 10 | 5 | crn | |- ran g |
| 11 | 10 | cuni | |- U. ran g |
| 12 | 8 | cuni | |- U. dom g |
| 13 | 12 5 | cfv | |- ( g ` U. dom g ) |
| 14 | 13 0 | cfv | |- ( F ` ( g ` U. dom g ) ) |
| 15 | 9 11 14 | cif | |- if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) |
| 16 | 7 1 15 | cif | |- if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) |
| 17 | 3 4 16 | cmpt | |- ( g e. _V |-> if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) |
| 18 | 17 | crecs | |- recs ( ( g e. _V |-> if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ) |
| 19 | 2 18 | wceq | |- rec ( F , I ) = recs ( ( g e. _V |-> if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) ) |