You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Madeleine Birchfield (Jan 17 2025 at 19:33):The statement that "every decidable entire relation contains a function" is equivalent to the axiom of choice if we assume excluded middle, since excluded middle implies that every relation is decidable. In the absence of excluded middle, what is the relation of this version of choice to the axiom of choice and to other weaker versions of the axiom of choice?
Mike Shulman (Jan 17 2025 at 21:00):Interesting question. To start with, it implies that every surjection onto a set with decidable equality has a section, which in turn implies the world's simplest axiom of choice.
Madeleine Birchfield (Jan 17 2025 at 21:48):Mike Shulman said:
To start with, it implies that every surjection onto a set with decidable equality has a section
This would also imply countable choice since the natural numbers have decidable equality.
Mike Shulman (Jan 17 2025 at 22:37):Yes, that's right, isn't it?
If has decidable equality and is a surjection, then is decidable and entire, and a function contained in it is a section of .
Mike Shulman (Jan 17 2025 at 22:40):I'm having a little trouble thinking of examples of decidable entire relations whose domain doesn't have decidable equality.
Morgan Rogers (he/him) (Jan 21 2025 at 09:35):You can build a hybrid case where part of the decidablility comes from the domain and part from the codomain by taking a coproduct of relations for the respective cases, but I also can't think of a more exotic way to construct a decidable relation.