MathOverflow update to my guarded domain theory question (https://mathoverflow.net/questions/504840/cauchy-completeness-in-ordered-families-of-equivalences-constructively)
I got two nice proofs that the principle that every weakly complete OFE is strongly complete is equivalent to countable choice in ZF. The proofs make essential use of LEM: they both show that a certain OFE that is not weakly complete must therefore not be strongly complete and therefore it must be the case that there exists a Cauchy sequence with no limit point, and this sequence is a choice function.
So I think constructively this proof can be used to show that if every weakly complete OFE is strongly complete then every countable family of inhabited sets does not not have a choice sequence. But I don't think that that doubly negated version is equivalent because I don't think you can use it to actually construct a limit point. So the problem isn't completely solved.
Max S. New ⚜️
npub1dm…g9dey
2025-12-19 20:54:51 UTC
Author Public Key
npub1dmn630rgl55pt7vgee6l930wfqjq6jry973hqf90fs6kgxztzd8qrg9deyPublished at
2025-12-19 20:54:51 UTCEvent JSON
{
"id": "33dc96d4b141be8f43c5f7393982a53b8ddb826231ab1be964c564e8a3823c50",
"pubkey": "6ee7a8bc68fd2815f988ce75f2c5ee48240d48642fa37024af4c3564184b134e",
"created_at": 1766177691,
"kind": 1,
"tags": [
[
"proxy",
"https://types.pl/users/maxsnew/statuses/115748221183513605",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.ditto.pub/"
]
],
"content": "MathOverflow update to my guarded domain theory question (https://mathoverflow.net/questions/504840/cauchy-completeness-in-ordered-families-of-equivalences-constructively)\n\nI got two nice proofs that the principle that every weakly complete OFE is strongly complete is equivalent to countable choice in ZF. The proofs make essential use of LEM: they both show that a certain OFE that is not weakly complete must therefore not be strongly complete and therefore it must be the case that there exists a Cauchy sequence with no limit point, and this sequence is a choice function.\n\nSo I think constructively this proof can be used to show that if every weakly complete OFE is strongly complete then every countable family of inhabited sets does not not have a choice sequence. But I don't think that that doubly negated version is equivalent because I don't think you can use it to actually construct a limit point. So the problem isn't completely solved.",
"sig": "1484f5038fdd022e0fefc3b01989e2d1b4b5166c19b5b084f42e0b968ed0176038e8652ea7ff187dc3ee7c0c1eae58173d3f6230694575651b0f9ea427e8ce52"
}