[pherq]

In this case, what you "throw out" are uncomputable (or non-recursive, depending on terminology you like) sets; i.e. sets for which the membership function is not decidable. Yes, there are an uncountable number of these sets, but they can't be defined in any useful way.

[zodiac]

For sure - as I understand it in most formulations you throw out lots of sets but keep all the finite sets of natural numbers, the set of even numbers, the set of prime numbers etc

One thing I never found satisfactory is that any axiom system like this has to define things in terms of decidability etc, so it's "more verbose" (or less axiomlike) than ZFC

[pherq]

This is a fair point.

I think the only axiom you need to rethink from ZF is powersets (since I think that's the only axiom that produces uncomputable sets from computable ones (ignoring the AC, briefly)). What you'd replace it with (some sort of one based on comprehension, presumably) I couldn't say though.

[baddox]

Indeed, if you consider a real number to just be a decimal representation formed by concatenating all the natural numbers in a set (not at all a rigourous construction of the reals, but hopefully sufficient for this argument), the equivalence is clear.

[zodiac]

I've always found dedekinds construction (where sqrt 2 is represented by the set of rationals {x in Q : x^2 < 2}) to be a nice natural place where powersets of countable infinite sets come up (in addition to being a great way to construct R)

[pherq]

I tend to prefer considering the sets to encode bitstrings (encode a set as sum(2 ^ -x for x in X)), but yes the equivalence between computable sets and computable numbers is straightforward.