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 ( 𝐹 , 𝐼 ) = recs ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cF | ⊢ 𝐹 | |
| 1 | cI | ⊢ 𝐼 | |
| 2 | 0 1 | crdg | ⊢ rec ( 𝐹 , 𝐼 ) |
| 3 | vg | ⊢ 𝑔 | |
| 4 | cvv | ⊢ V | |
| 5 | 3 | cv | ⊢ 𝑔 |
| 6 | c0 | ⊢ ∅ | |
| 7 | 5 6 | wceq | ⊢ 𝑔 = ∅ |
| 8 | 5 | cdm | ⊢ dom 𝑔 |
| 9 | 8 | wlim | ⊢ Lim dom 𝑔 |
| 10 | 5 | crn | ⊢ ran 𝑔 |
| 11 | 10 | cuni | ⊢ ∪ ran 𝑔 |
| 12 | 8 | cuni | ⊢ ∪ dom 𝑔 |
| 13 | 12 5 | cfv | ⊢ ( 𝑔 ‘ ∪ dom 𝑔 ) |
| 14 | 13 0 | cfv | ⊢ ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) |
| 15 | 9 11 14 | cif | ⊢ if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) |
| 16 | 7 1 15 | cif | ⊢ if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) |
| 17 | 3 4 16 | cmpt | ⊢ ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) |
| 18 | 17 | crecs | ⊢ recs ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ) |
| 19 | 2 18 | wceq | ⊢ rec ( 𝐹 , 𝐼 ) = recs ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐼 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ) |