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 e. _V |-> if ( g = (/) , I , if ( Lim dom g , U. ran g , ( F ` ( g ` U. dom g ) ) ) ) ) )

Detailed syntax breakdown

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 ) ) ) ) ) )