ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-frec Unicode version

Definition df-frec 6008
Description: Define a recursive definition generator on  om (the class of finite ordinals) with characteristic function  F and initial value  I. 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 frec operation (especially when df-recs 5950 that it is built on is also eliminated). But once we get past this hurdle, definitions that would otherwise be recursive become relatively simple; see frec0g 6013 and frecsuc 6021.

Unlike with transfinite recursion, finite recurson can readily divide definitions and proofs into zero and successor cases, because even without excluded middle we have theorems such as nn0suc 4354. The analogous situation with transfinite recursion - being able to say that an ordinal is zero, successor, or limit - is enabled by excluded middle and thus is not available to us. For the characteristic functions which satisfy the conditions given at frecrdg 6022, this definition and df-irdg 5987 restricted to  om produce the same result.

Note: We introduce frec with 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 Mario Carneiro and Jim Kingdon, 10-Aug-2019.)

Assertion
Ref Expression
df-frec  |- frec ( F ,  I )  =  (recs ( ( g  e.  _V  |->  { x  |  ( E. m  e.  om  ( dom  g  =  suc  m  /\  x  e.  ( F `  (
g `  m )
) )  \/  ( dom  g  =  (/)  /\  x  e.  I ) ) } ) )  |`  om )
Distinct variable groups:    x, g, m, F    x, I, g, m

Detailed syntax breakdown of Definition df-frec
StepHypRef Expression
1 cF . . 3  class  F
2 cI . . 3  class  I
31, 2cfrec 6007 . 2  class frec ( F ,  I )
4 vg . . . . 5  setvar  g
5 cvv 2574 . . . . 5  class  _V
64cv 1258 . . . . . . . . . . 11  class  g
76cdm 4372 . . . . . . . . . 10  class  dom  g
8 vm . . . . . . . . . . . 12  setvar  m
98cv 1258 . . . . . . . . . . 11  class  m
109csuc 4129 . . . . . . . . . 10  class  suc  m
117, 10wceq 1259 . . . . . . . . 9  wff  dom  g  =  suc  m
12 vx . . . . . . . . . . 11  setvar  x
1312cv 1258 . . . . . . . . . 10  class  x
149, 6cfv 4929 . . . . . . . . . . 11  class  ( g `
 m )
1514, 1cfv 4929 . . . . . . . . . 10  class  ( F `
 ( g `  m ) )
1613, 15wcel 1409 . . . . . . . . 9  wff  x  e.  ( F `  (
g `  m )
)
1711, 16wa 101 . . . . . . . 8  wff  ( dom  g  =  suc  m  /\  x  e.  ( F `  ( g `  m ) ) )
18 com 4340 . . . . . . . 8  class  om
1917, 8, 18wrex 2324 . . . . . . 7  wff  E. m  e.  om  ( dom  g  =  suc  m  /\  x  e.  ( F `  (
g `  m )
) )
20 c0 3251 . . . . . . . . 9  class  (/)
217, 20wceq 1259 . . . . . . . 8  wff  dom  g  =  (/)
2213, 2wcel 1409 . . . . . . . 8  wff  x  e.  I
2321, 22wa 101 . . . . . . 7  wff  ( dom  g  =  (/)  /\  x  e.  I )
2419, 23wo 639 . . . . . 6  wff  ( E. m  e.  om  ( dom  g  =  suc  m  /\  x  e.  ( F `  ( g `
 m ) ) )  \/  ( dom  g  =  (/)  /\  x  e.  I ) )
2524, 12cab 2042 . . . . 5  class  { x  |  ( E. m  e.  om  ( dom  g  =  suc  m  /\  x  e.  ( F `  (
g `  m )
) )  \/  ( dom  g  =  (/)  /\  x  e.  I ) ) }
264, 5, 25cmpt 3845 . . . 4  class  ( g  e.  _V  |->  { x  |  ( E. m  e.  om  ( dom  g  =  suc  m  /\  x  e.  ( F `  (
g `  m )
) )  \/  ( dom  g  =  (/)  /\  x  e.  I ) ) } )
2726crecs 5949 . . 3  class recs ( ( g  e.  _V  |->  { x  |  ( E. m  e.  om  ( dom  g  =  suc  m  /\  x  e.  ( F `  ( g `
 m ) ) )  \/  ( dom  g  =  (/)  /\  x  e.  I ) ) } ) )
2827, 18cres 4374 . 2  class  (recs ( ( g  e.  _V  |->  { x  |  ( E. m  e.  om  ( dom  g  =  suc  m  /\  x  e.  ( F `  ( g `
 m ) ) )  \/  ( dom  g  =  (/)  /\  x  e.  I ) ) } ) )  |`  om )
293, 28wceq 1259 1  wff frec ( F ,  I )  =  (recs ( ( g  e.  _V  |->  { x  |  ( E. m  e.  om  ( dom  g  =  suc  m  /\  x  e.  ( F `  (
g `  m )
) )  \/  ( dom  g  =  (/)  /\  x  e.  I ) ) } ) )  |`  om )
Colors of variables: wff set class
This definition is referenced by:  freceq1  6009  freceq2  6010  frecex  6011  nffrec  6012  frec0g  6013  frecfnom  6016  frecsuclem1  6017  frecsuclem2  6019
  Copyright terms: Public domain W3C validator