Not an answer, and not taking position, but this tension between a pedagogical goal and a "reference work" goal has already appeared (e.g. the binomial theorem is now proved in set.mm for general rings, and it is proved that complex numbers form a ring, but the binomial theorem for complex numbers is not proved as a direct corollary of these two facts), and this tension is bound to appear again: these goals are simply not compatible (after all, except for restricted fields, most textbooks are not reference works, and the brilliant reference work by Bourbaki would do a terrible textbook).
By the way: I see that there are things on well-founded recursion in JBN's mathbox (http://us2.metamath.org/mpeuni/mmtheorems.html). How do they compare ? Benoit On Sunday, August 2, 2020 at 8:06:46 AM UTC+2 [email protected] wrote: > On 8/1/20 2:41 PM, Norman Megill wrote: > > > 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? > > I guess the answer is that I got through a major in undergraduate > mathematics, and a certain amount of recreational mathematics, where > recursion was pretty much assumed and treated informally. This would > mostly be recursion on natural numbers. I had heard of transfinite > recursion, but not well-founded recursion (at least, not by that name, I > couldn't say for sure whether there was some kind of argument applied > informally which amounted to well-founded recursion). I'm not sure we > even got as far as handwaving at something vaguely called the "Recursion > Theorem". So in a way I'm not a good test case, because I didn't really > learn either kind of recursion, at least not with rigor. > > Given this, having to formalize recursion for iset.mm was a bit of a > rude awakening. Having the set.mm treatment was helpful, but it breaks > down after tfrlem9 . And although I have found constructive set thoery > references (maybe not exactly textbooks, but close enough in the sense > that they can often be formalized without major changes) for things like > Dedekind cuts, complex division, and others, I found nothing of the sort > for recursion. > > Sorry I'm not sure that saying "the number of people who really worry > about how recursion works is much smaller than the number of people who > use recursion without really thinking about it too hard" really answers > your question. But I do share a certain amount of what seems to be your > caution - in terms of whether building in too much generality would make > it even less clear how ordinal recursion is working. > > > -- 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/9fc99246-138d-4e9c-bef5-30d43569db57n%40googlegroups.com.
