On: The field of “useful reals” between rational and r...

[lonelappde]

Finite descriptions are countable. Axiom of Countable Choice is not counterintuitive like Axiom of (Uncountable) Choice.

You can order the set of all definitions, by prepending each definition with its length and then using the ordering (numerical order, alphabetical order).

[OscarCunningham → lonelappde]

That doesn't even need Countable Choice. You only need any form of Choice when you can't explicitly specify an order, which you did.