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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/3f017efb-c8d2-4888-a2de-229612d96392o%40googlegroups.com.
