Timeline for Well-foundedness: classical equivalence of no infinite descent and accessibility
Current License: CC BY-SA 4.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 18, 2022 at 17:11 | comment | added | daniel gratzer | @kyodralliam Very cool! I've added a paragraph to the above answer. | |
| Mar 18, 2022 at 17:11 | history | edited | daniel gratzer | CC BY-SA 4.0 |
added 307 characters in body
|
| Mar 18, 2022 at 16:09 | comment | added | Andrej Bauer | @kyodralliam: Very good, you beat me to it in formalization :-) The answer should be updated with a refefence to Kenji's proof. | |
| Mar 18, 2022 at 12:44 | comment | added | kyo dralliam | Dependent choice is also necessary, see here for a proof in Coq. | |
| Mar 18, 2022 at 10:27 | vote | accept | Théo Winterhalter | ||
| Mar 18, 2022 at 9:03 | comment | added | François G. Dorais | This argument more precisely that $\mathsf{idc}(A,R,a) \iff \neg\mathsf{Acc}(A,R,a)$. LEM is necessary to prove this: Take $A=\{a\}$ then $\mathsf{idc}(A,R,a) \iff a \mathrel{R} a$ and $\mathsf{Acc}(A,R,a) \iff \lnot(a \mathrel{R} a)$. Since $R$ is arbitrary, LEM follows from the equivalence. The stated equivalence $\lnot\mathsf{idc}(A,R,a) \iff \mathsf{Acc}(A,R,a)$ appears to be a bit more subtle. | |
| Mar 17, 2022 at 21:58 | history | answered | daniel gratzer | CC BY-SA 4.0 |