Well-founded recursion without infinity #4296
Conversation
| nffrecs.3 $e |- F/_ x F $. | ||
| $( Bound-variable hypothesis builder for the well-founded recursion | ||
| generator. (Contributed by Scott Fenton, 23-Dec-2021.) $) | ||
| nffrecs $p |- F/_ x frecs ( R , A , F ) $= |
There was a problem hiding this comment.
Probably this and later theorems should be put in deduction form eventually, for wide usability. This can of course be done later, and by others. Since applications are rather at a fundamental level, the need of being contextual is less frequent, so the need for deduction form is less acute.
There was a problem hiding this comment.
(And that particular theorem is not a very good example, since the need of deduction form would be very rare: we have the choice to use a fresh variable x; for other theorems, there may be a need.)
|
Also: have you had a look at BNJ's mathbox ? If the work is related, we should find a place to add some credit to him. |
|
Sorry, who's BNJ? You're the only BJ I can find in set.mm |
Sorry, I meant "Jonathan Ben-Naim". Most of his theorems are labeled He's apparently a former contributor and his theorems date from before I even know of metamath. His mathbox has sections on recursion too. |
|
Hm, he and I seem to have developed the same theorems around the same time. We even used the same reference! His theorems only cover the case that requires infinity though. I'm not completely sure what to do about credit here. |
Continuation of #4290. This MR brings in well-founded recursion over a partial order. This can be used to revise wrecs and shorten a lot of theorems there.