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/ee3796a4-ac66-80d3-76f1-e017414a9886%40panix.com.
