>>12380033Enumerable: X injects into N.
Countable: N maps onto X
Subcountable: A subset I of N maps onto X.
If your axiom prove that all non-finite subsets of N are in bijection with N, then the last two are the same. If it doesn't, then you have the chance of more constructive semantics of "countable".
E.g. all strings X are countable, say via a bijection b:N->X.
Some strings Y subset X correspond to compiling C++ programs that halt when executed with main().
It's not decidable for all x in X (i.e. not decidable in general) whether a given x is in Y.
There is now an infinite index set I subset N such that b(I)=Y, basically the preimage for b of Y.
Of course n in N being in I is not decidable either, otherwise we could decide b(n) in Y.
So Y is subcountable, via I.
And so I or Y are not "actually countable", in the sense that there's no counting algorithm. I is an uncountable subset of N. As in, nobody will ever find an algorithm that maps n in N to just all the elements in i.
Of course, ZF proves there is a bijection function from I N, but that's just because of LEM. It's not "ackshually true" that Y is countable, you can't count Y. It's just a ZF theorem that Y is countable.
(Apart from godly bijection functions, ZF+Choice also proves there's choice functions for all non-empty sets and ZF+CH proves there's orderings functions between 2^N and omega_1, but all those functions are arguably just axiomatized into the theory for convenience.)
>>12380137iirc that's called modulated Cauchy and is what Bishop used
