On Wednesday, July 29, 2020 at 11:09:40 AM UTC-4, Scott Fenton wrote: > > 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.
On Thu, 30 Jul 2020 07:51:36 -0700 (PDT), Norman Megill <[email protected]> wrote: > This is nice work, and I am in favor of moving it into the main set.mm. Excellent, I agree. I think that all the Metamath 100 theorems (and their dependencies) should be moved into the main body eventually, possibly after some reviews & clean-ups where important. > > 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. Both alternatives have really good arguments. If we keep the definitions as they are, I think we need to add a discussion about this in the comments (with cross-references to make the discussion easier to find). And, of course, include the proof of the relationship in the main body. --- David A. Wheelr -- 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/E1k1Ati-0002it-LN%40rmmprod06.runbox.
