The set
${\mathcal F}=\{\{\},\{0\},\{1\},\{0,1\},\dots,\{4,5,73\},\dots\}$
of finite subsets of $\mathbb N$ is one we can do a lot of math with and it is in fact in bijection with $\mathbb N$. Say we don't want to do analysis and anything to do with the real numbers. But we want to keep all subsets of $\mathbb N$ and ${\mathcal F}$. We don't demand to have all function spaces as sets.
Pre-question: What's a strong conventional set theory providing us with this?
Maybe there's no good wellordering in that sense. Okay then,
- what do I have to drop from ZF (having the axiom of infinity) so that the full powerset axiom isn't implied, but all subsets of $\mathbb N$ and ${\mathcal F}$ exists.
I know that one the lower end somewhere is Kripke–Platek set theory, but I don't know where.
Let me come from another direction.
- Let's consider, within ZFC, the set including the class of all subsets of $\mathbb N$ and ${\mathcal F}$ exists. (That class is in ZFC a proper set, of course). Which axioms of weaker forms of axioms of ZFC do hold in this class?
It might be that I'm just searching for the right weak form of replacement.
Well. The power set axiom.
If you don't drop the power set axiom, then the power set axiom is implied. But without it, while we don't have a full power set, we can still use Replacement and the fact that there is a very nice enumeration of all the finite subsets of the natural numbers to produce the set of all finite subsets of $\Bbb N$.
And indeed if you consider $H(\omega_1)$ which is the set of all $x$ such that the transitive closure of $\{x\}$ is countable, then $H(\omega_1)$ satisfies all the axioms of $\sf ZF$ except the power set axiom, and in addition "every set is countable".
Regarding the axiom of choice, depending on how you formulate it, it should follow naturally from the assertion "All sets are countable", as long as you have unions and a reasonable separation schema. If you have a family of sets, and the family is countable, and all its members are countable, and the union is a set, then the union is countable. Using the definition of countable and the separation schema, you can now define the choice function to be the obvious thing: the least indexed element of the union from each family.
You can redefine countable to mean "can be linearly ordered such that every proper initial segment is finite", which will certainly give you a notion of countability without talking about functions and natural numbers. In that case I don't see directly how you can prove the existence of a choice function; but you can prove a well-ordering theorem, so that form of choice holds.
(And in any case, we want strong fragments of ZF, so the last paragraph is irrelevant.)