So you're proposing leaving the tfr* development in place, just turning df-recs into a dfrecs3 or something? I can do that. In fact, I originally had that as a direct proof back before df-recs existed. I'll make the relevant mods and do a pull request.
I'm still interested in hearing about people's experiences with recursion theorems. I'd eventually like to develop a set of recursion theorems that use the transitive closure, so we can say "R Fr A" instead of "R We A". That requires Infinity, so it wouldn't replace any of the current developments. However, it plays well with my long-term goal of formalizing the surreal numbers in MM. On Sat, Aug 1, 2020 at 5:41 PM Norman Megill <[email protected]> wrote: > On Thursday, July 30, 2020 at 12:53:08 PM UTC-4, Scott Fenton wrote: >> >> 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. >> >> > I like your WFR work and would like to see it in the main set.mm. But I'm > still concerned that some people may want to see the traditional textbook > ordinal transfinite recursion. > > While harmonizing it with the NF development is a nice goal in principle, > we also need to look at what is best for set.mm/ZFC. For example, set.mm > doesn't build on top of the intuitionistic set theory of iset.mm but has > an independent classical development that more closely follows textbook ZFC > and its axioms. > > Can you give some more detail how you envision replacing the ordinal TFR? > What parts of the current ordinal development would be discarded? Where do > you propose placing the WFR development? > > Is it possible to set up the two developments in a way that we can switch > between them by doing something like swapping df-recs and tfrALTlem as the > recs definition (maybe with some auxiliary lemmas to make this easier)? > That could provide an alternative for the reader interested in the textbook > ordinal development (after thus modifying set.mm and regenerating the web > pages locally). As long as we have a way to go back without much difficulty > if we change our minds later, I'll accept making tfrALTlem the official > definition as you propose. That will let us postpone a decision to delete > the ordinal TFR. > > It would be interesting to hear how other people learned transfinite > and/or well-founded recursion, and which is considered "harder" for the > beginner. Is there a reason ordinal TFR is the one that (I think) is > mostly used? > > 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/d061c9e3-58bc-41d1-a338-13f441fa1c60o%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/d061c9e3-58bc-41d1-a338-13f441fa1c60o%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-p0R%2BoSta8LsG%2BvCSc3ntw4cbfNQrKHwBu%2B-WttJUP6Q%40mail.gmail.com.
