Total ordering needed for recursion ?

[benjub]

That's more of a question, but it's easier to ping both @scott-fenton and @sctfn here.

The theorem giving the value of a function defined by recursion (https://us.metamath.org/mpeuni/wfr2.html) requires that the relation be a total order: it is

wfr2.1 $e |- R We A $.
wfr2.2 $e |- R Se A $.
wfr2.3 $e |- F = wrecs ( R , A , G ) $.
wfr2 $p |- ( X e. A -> ( F ` X ) = ( G ` ( F |` Pred ( R , A , X ) ) ) ) $=

but We is actually the conjunction of well-foundedness and total ordering (see https://us.metamath.org/mpeuni/df-we.html).

That requirement of total ordering seems extraneous to me: probably a partial order suffices, and even that may be circumvented, with perhaps a slight adaptation of the definition. Is that correct ?

After a quick look at the proof, it seems that the only place where total ordering is used is https://us.metamath.org/mpeuni/tz6.26.html, but total ordering can apparently be removed from that statement. Indeed, it uses https://us.metamath.org/mpeuni/wereu2.html which proves existence and uniqueness of a minimal element, but only requires existence, not uniqueness, and existence does not need total ordering.

Since the adaptation of the chain of proofs from that point up to wfr2 would a bit long, before spending some time on it, maybe Scott if you remember your proof you may shed some light on these choices ?

[jkingdon]

Unless I'm missing something, this is similar to the way that iset.mm defines recursion on constructive ordinals (which do not have a total ordering). There are at least two variations there, on all ordinals (for example: https://us.metamath.org/ileuni/tfri1.html ) or up to a point (for example, just on natural numbers) ( https://us.metamath.org/ileuni/tfrcl.html ).

[sctfn]

So, I've actually done this work in my mathbox. You can either use a well founded partial ordering, or you can assume Infinity and dispense with the partial requirement. However, as a practical matter, you need to change the characteristic function to take the current value (ie, F(X,Pred(X)) instead of just F(Pred(X))). This is because without total ordering X is no longer dictated by Pred(X). For details, see my work surrounding df-frecsOn Oct 12, 2024, at 1:53 PM, Jim Kingdon ***@***.***> wrote: Unless I'm missing something, this is similar to the way that iset.mm defines recursion on constructive ordinals (which do not have a total ordering). There are at least two variations there, on all ordinals (for example: https://us.metamath.org/ileuni/tfri1.html ) or up to a point (for example, just on natural numbers) ( https://us.metamath.org/ileuni/tfrcl.html ). —Reply to this email directly, view it on GitHub, or unsubscribe.You are receiving this because you were mentioned.Message ID: ***@***.***>

[sctfn]

Gah, that's what I get for typing on a phone. The characteristic function without total ordering is F(X) = G(X,F|`Pred(X)) as opposed to F(X) = G(F|`Pred(X))

…

On Sat, Oct 12, 2024 at 2:12 PM Scott Fenton ***@***.***> wrote: So, I've actually done this work in my mathbox. You can either use a well founded partial ordering, or you can assume Infinity and dispense with the partial requirement. However, as a practical matter, you need to change the characteristic function to take the current value (ie, F(X,Pred(X)) instead of just F(Pred(X))). This is because without total ordering X is no longer dictated by Pred(X). For details, see my work surrounding df-frecs On Oct 12, 2024, at 1:53 PM, Jim Kingdon ***@***.***> wrote:  Unless I'm missing something, this is similar to the way that iset.mm defines recursion on constructive ordinals (which do not have a total ordering). There are at least two variations there, on all ordinals (for example: https://us.metamath.org/ileuni/tfri1.html ) or up to a point (for example, just on natural numbers) ( https://us.metamath.org/ileuni/tfrcl.html ). — Reply to this email directly, view it on GitHub <#4279 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAHTIWA4UCO2I4TMI3DX5R3Z3FOY3AVCNFSM6AAAAABP2NLRXGVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDIMBYGY2DENJQGI> . You are receiving this because you were mentioned.Message ID: ***@***.***>

[benjub]

Perfect ! You're right, the parameter is necessary, and actually it is always more flexible to have it in the first place, even when it's technically not required. Your mathbox treatment is a strict improvement over the main part, and eventually it should be moved to Main. For now, I will benefit from the fact that your last name comes before mine in the alphabet !

Jim: I see, that's a nice way to circumvent the need for a total ordering in the case of ordinals and membership. This seems to follow roughly the same method as Scott's. The key property is that membership is extensional, since as Scott notes, you need Pred(X) to determine X.

Thanks to both.

[benjub]

Work is ongoing to move the relevant parts to Main: #4290 #4296

When done, we'll close this issue.

[sctfn]

Ready to close this one?

[benjub]

We still have to make a PR to acknowledge the work of Ben-Naim. I'll try to propose something.

I'd like to ask another question here: as you noted, extensionality of a relation is important if you want to be able to define recursion without taking the "current set" as parameter. Do you have a plan to introduce extensional relations ?

[sctfn]

Sorry, this has been a hectic week, I totally missed this.

I don't currently have plans to work with extensional relationships, but that's certainly an interesting possibility. Strictly there's nothing in the recursion theorems that uses the current element parameter - it's only in there for convenience with actual use.

[benjub]

Sorry, this has been a hectic week, I totally missed this.

I don't currently have plans to work with extensional relationships, but that's certainly an interesting possibility. Strictly there's nothing in the recursion theorems that uses the current element parameter - it's only in there for convenience with actual use.

What I mean, is really weakening the condition "well-order" to the condition "extensional and well-founded" in all these theorems.