Thanks a lot, Toby! This looks very good.

]]>I went ahead and implemented Mike's more systematic terminology, at least for purposes of this article. But I think that it's clear that ’countably indexed’ is the most interesting notion of countability.

I also rearranged the examples and made sure that they all used the correct terminology to be constructive, or noted when they were not constructive. And I added some interesting history from Wikipeda, which is hopefully accurate.

]]>More different constructive terms, and some results about them.

]]>I have now changed the definitions as noted in the previous comment. But more edits may be useful, such as adding ‘enumerable’ for an inhabited countable set.

]]>One issue is that even classical mathematicians are not consistent with their definitions. I was about to say that Frank'a in #2 had learnt the classical definitions almost exactly reversed from how I learnt them, but then I realized that she wrote ‘enumerable’ rather than ‘denumerable’, which averted the crisis.

So classically, we have 3 classes of cardinalities, which I'll list from smallest to largest and describe up to bijection for brevity:

- Denumerable: all of $\mathbb{N}$;
- Enumerable: a quotient of $\mathbb{N}$;
- Countable: a subset of $\mathbb{N}$.

(Note that (2) = (3) & inhabited, classically.) I have given these names, and my justification for naming them as I have is that they're the only meanings (up to classical equivalence, which I take to include full AC) that I can recall seeing for (1) and (2); an additional justification for (3) is that it's precisely the negation of ‘uncountable’ (classically).

Having settled the question of classical terminology (if I have), we can now consider further bifurcations of definitions in constructive math, and see if maybe one of them works best. If not, then we might have to introduce adjectives.

Now, about the most general definition possible is a subquotient of $\mathbb{N}$. But the problem with that is that $\mathbb{R}$ can be a subquotient of $\mathbb{N}$! (It is Russian constructivism; everyone agrees that the computable real numbers form a subquotient of $\mathbb{N}$, and the Russians believe that every real number is computable.) Since the concept of countability was first developed by Cantor to distinguish $\mathbb{N}$ from $\mathbb{R}$, we should probably preserve the idea that $\mathbb{R}$ is uncountable. So here is where detachability comes in; $\mathbb{R}$ cannot be a *detachable* subquotient of $\mathbb{N}$ (meaning that the subset membership is decidable, with no restriction on the equivalence relation). The reason is that Cantor's original proof of the uncountability of $\mathbb{R}$ works constructively as long as you start with a detachable subset. (Some care is needed to make his proof constructive, but not much.)

So that explains why I defined a countable subset as a detachable subquotient of $\mathbb{N}$. But elsewhere in the article, I was thinking of a different definition: not a quotient of *any* detachable subset, but a quotient of a detachable *lower set*! This is what you need to prove that a countable set is empty or inhabited, for example. It also has no effect on the definition of *uncountable*, essentially by Frank'a's trick from #5 and #6 above. So if I change ‘subset’ to ‘lower set’ at appropriate places in the article, then this will fix the error. (I'll also change ‘decidable’ to ‘detachable’, to avoid the clash of terminology for subsets of $\mathbb{N}$ that Frank'a identified in #7.) Ultimately, Frank'a's trick proves that an inhabited detachable subquotient of $\mathbb{N}$ is a quotient of $\mathbb{N}$, which helps a lot of things collapse that might otherwise be distinguishable. In particular, that countable = empty or enumerable is still true.

I would guess that I got the detachable lower subquotient from Troeslstra & van Dalen (1988), but they don't seem to have used it (or anything else officially) as a definition of ‘countable’. They (or someone) impressed upon me its significance for the definition of uncountability.

]]>Re: #7, this may be part of why some people say “detachable” instead for a subset having the property that everything is either in it or not in it.

By analogy to “finite” and “finitely indexed”, I would be inclined to define a set as “countable” if it is in bijection with $\mathbb{N}$ and “countably indexed” if it admits a surjection from $\mathbb{N}$. I don’t remember ever seeing this business of detachable subsets of $\mathbb{N}$ appearing in the notion of countability. Toby, if you’re listening, do you have references for it?

]]>btw the above illustrates another terminological problem which mostly goes unnoticed: the definition of ‘decidable subset’. in classical complexity theory, a subset of N is decidable iff its membership function is a total *recursive* function. this is however not so in constructive mathematics, in constructive mathematics it suffices to have a total membership function (since functions are considered to be evaluable for any n).

this often leads to confusion, especially when giving talks…

for a constructive mathematician, given $\alpha$ in Baire space, the set S = {n | $\alpha$(n)=1} is decidable…

for defining ‘countable’ this terminological confusion can be prevented by using the proposed definition of enumerability and ($\ast$) above.

]]>if we let the definitions be

i’) a set S is countable iff there is a surjection from a decidable subset of N to S

ii) a set S is enumerable iff there is a surjection from N to S

then we have the following correspondence:

(${\ast}$) a set S is countable iff $\{-1\}\bigcup\,$S is enumerable.

proof:

-> let D be decidable, let f be a surjection from D to S, let g be an enumeration of $\{-1\}\bigcup\,$D, put f(-1)=-1, then h=f$\circ$g is an enumeration of $\{-1\}\bigcup\,$S.

<- let f be an enumeration of $\{-1\}\bigcup\,$S, then D = {n| f(n) in N} is decidable, and f restricted to D is a surjection from D to S.

this illustrates to me that enumerability is more useful than the current definition of ’countable’.

]]>the current definition of ’countable’ in countable set is lacking, i feel, in the following way.

from time to time when trying to define an enumerable cover of a topological space, or an enumerable basis of opens, or an enumerable filtering set, one really wants to have a concrete enumeration, which one can start with, not depending on (the undecidable issue of) whether some decidable set is inhabited or not.

a simple trick that i have had occasion to use:

if S is a decidable subset of N, then $\{-1\}\bigcup\,$S is enumerable.

the current definition of ’countable’ in countable set does not differentiate between those sets that can be enumerated (which in all practical situations is a big plus) and those for which it is unknown.

less importantly, on the terminology side, the definition implies that many sets which in intuitionistic math are called subfinite, are countable according to nLab.

what’s in a name, it doesn’t matter much to me, but i do think that the concept of ’enumerability’ needs to be added.

]]>Thanks. If you think there is room to clarify any remaining subtlety in the entry, please consider doing so.

]]>The nlab entry defines countable constructively as

$S$ is countable if there exists a surjection from a decidable subset of $\mathbf{N}$ to $S$

I agree that under this definition inhabitedness is not decidable, but the argument about the Goldbach conjecture is only a “weak counterexample” (as Brouwer calls it) in that existence of even non-Goldbach numbers > 4 might well be decidable. A proof of non-decidability of inhabitedness of decidable sets of integers can be given by showing that it implies decidability of the halting problem.

]]>the way i learned these definitions is thus:

i) a set S is countable iff there is a bijection from N to S

ii) a set S is enumerable iff there is a surjection from N to S

that means that in my dictionary countable and enumerable sets are inhabited, and that decidable subsets of N need not be enumerable, but: every inhabited decidable subset of N is enumerable.

the example D={n\in N | 2n+6 is not the sum of two odd primes} is decidable, but so far not enumerable, in my book.

]]>Somebody sent me an email with the following comment on the entry *countable set*. I am not in position to react to this, maybe some expert here could reply. The sentence being quoted originates from revision 1 of the entry.

Forwarded message:

]]>“We do have, however, that a countable set is either empty or inhabited, which is classically trivial but need not hold constructively for every set.”

(https://ncatlab.org/nlab/show/countable+set)

The set D={n\in N | 2n+6 is not the sum of two odd primes} is decidable, hence countable. However we cannot decide whether it is empty or inhabited. (We could decide it if we assumed LPO, for instance.)

Do you agree?