I don't think much is lost by making well-founded recursion the basic system. The development of the well-founded theorems actually parallels the transfinite case quite closely. It merely emphasizes the difference between a set and it's predecessor set, which I think is a valuable distinction to make. I'm working on getting the Replacement-free versions of the theorems into my branch now, but I don't anticipate any large problems.
There's also the fact that this will more closely follow the NF version of recursion that I'm trying to get underway. In that version, we have to distinguish between a set and its predecessor set, since there are no von Neumann ordinals to fall back on. On Thu, Jul 30, 2020 at 10:51 AM Norman Megill <[email protected]> wrote: > On Wednesday, July 29, 2020 at 11:09:40 AM UTC-4, Scott Fenton wrote: >> >> Hi all, >> >> I'd like to move my theorem fsumkthpow (giving the value of the finite >> sum of powers) into the main body of Metamath, since it's a 100 theorem. >> However, that depends on the definition of Bernoulli polynomials, which I >> define using my well-founded recursion theorems. This is a fairly large >> body of theorems, so I'd like to get opinions before moving the three >> sections that this requires up. >> > > This is nice work, and I am in favor of moving it into the main set.mm. > > >> >> If there's support for this, is there support for reworking transfinite >> recursion to be a special case of well-founded recursion? tfr1 through 3 >> can be easily expressed by setting recs ( F ) = wrecs ( _E , On , F ). I'd >> like to make this the official definition of recs, since it expresses that >> the important part of recursion is well-foundedness, not anything special >> about the ordinals themselves. Any thoughts? >> > > Certainly we can state "recs ( F ) = wrecs ( _E , On , F )" as a theorem > (it looks like it is already there, ~tfrALTlem) that provides an alternate > definition called ~dfrecs3. (There is already a ~dfrecs2.) > > What concerns me is that the present ordinal-based development is very > close to textbooks (most textbooks I think, although I'm not sure), with > detailed references to Takeuti-Zaring in particular that match the textbook > almost exactly. Transfinite recursion is already a somewhat difficult > topic, in a way the first "deep" theorem about ordinals, and I'm wondering > if it makes sense to discard that in favor of the more general well-founded > recursion. In other words, would we be throwing away a useful didactic > tool? I'm not sure how many people have used the present ordinal tfr to > assist self-learning; one I know of was Alan Sare. > > I'd like to see more discussion of this point. > > Norm > > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/3f017efb-c8d2-4888-a2de-229612d96392o%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/3f017efb-c8d2-4888-a2de-229612d96392o%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CACKrHR_UM_mqy2%2B9Z%2BBYcNC3s_1ZCq3eJnwWPJOR0x-h2c2wyg%40mail.gmail.com.
