By the way: logicians sometimes pedantically draw a distinction between ‘recursion’ and ‘induction’: induction is for proving things; recursion is for defining

By the way: logicians sometimes pedantically draw a distinction between ‘recursion’ and ‘induction’: induction is for proving things; recursion is for defining things. And it’s not just terminological: the difference becomes very important when you realise one needs to prove that recursion is possible (that is, function definitions by recursion on a well-ordered set are well-defined) by induction. So one actually comes logically before the other. I guess to truly determine whether they’re distinct concepts you’d have to exhibit some model of set theory that supports recursion but not induction, or something. But that’s beyond me.