Timeline for Strictly-monotone "max" operation for constructive Brouwer-trees?
Current License: CC BY-SA 4.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 9, 2022 at 18:42 | comment | added | Andrej Bauer |
Let nat : Nat → Ord be the obvious embedddding, and let ω = limit nat. How do you show that omega ≤ limit (λ k → 2 * k)?
|
|
| Aug 9, 2022 at 18:40 | comment | added | Andrej Bauer |
Successor need not be monotone constructively, what makes you think you've got the correct definition of ≤?
|
|
| Aug 9, 2022 at 18:38 | comment | added | Andrej Bauer | From the description of your functions and arguments it does not yet follow that you've got termination. It would be useful to see more details. | |
| Jun 3, 2022 at 3:46 | answer | added | Dan Doel | timeline score: 6 | |
| Jun 2, 2022 at 5:15 | comment | added | ionchy |
This mastodon.vierkantor.com/@Vierkantor/108406129582981803 pointed out that if f 0 = zero; f (n+1) = succ (f n) then lim (λn. succ (f n)) is equal (isomorphic? idk) to lim f (i.e. ω), which is strictly smaller than succ (lim f), so if succ (lim f) ≤ lim (λn. succ (f n)) is where you ended up naturally, and that's refutable, maybe your max is wrong? Or maybe any definition of max just isn't monotone?? Better ask a set theorist
|
|
| Jun 2, 2022 at 0:13 | comment | added | Li-yao Xia | You may need the max to make the first call, but once inside the recursive function you only need the upper bound to decrease, not necessarily to remain equal to the max. | |
| Jun 1, 2022 at 22:42 | comment | added | Joey Eremondi | @Li-yaoXia But how would I generate the bounds for recursive calls without a max function? | |
| Jun 1, 2022 at 22:23 | comment | added | Li-yao Xia | Rather than computing the max, have you considered only tracking an upper bound on both arguments? | |
| Jun 1, 2022 at 21:32 | history | edited | Joey Eremondi | CC BY-SA 4.0 |
added 255 characters in body
|
| Jun 1, 2022 at 20:35 | history | asked | Joey Eremondi | CC BY-SA 4.0 |