Hereditarily finite/countable/small sets in ZF I want to determine which ZF axioms are satisfied by each of these.
HF
It seems obvious to me that extension, empty-set, pair-set, union, and power-set hold for these. I'm not sure about replacement and separation. The $\Sigma_0$ versions of these should hold but universal quantifiers might be a problem? Can we get an infinite set from separation and replacement if we're allowed to access the whole universe? On the other hand if this was the case, why would we ever need the infinity axiom in ZF ...
The infinity axiom itself clearly doesn't hold. Wikipedia says that HF is a model of ZF where the infinity axiom is replaced by its negation. So without negated infinity it wouldn't be a model?
This also implies that foundation holds but can't I have $x\in x$ with $x$ heriditarily finite? 
HC
Again it seems clear to me that extension, empty-set, pair-set, and union hold.
Power-set does not hold as the power set of the natural numbers is not countable while infinity holds as the natural numbers themselves are countable.
Wikipedia says HC is a model of Kripke-Platek with infinity if the axiom of countable choice is assumed in the metatheory. Why exactly do we need choice, or what happens without choice? Why can we only have $\Sigma_0$ versions of separation and replacement, what would go wrong if we take the strong versions? Similarly what's the problem with foundation? (KP uses $\in$-induction instead which is weaker)
On a side note, Wikipedia also says the following:

A set is hereditarily countable if and only if it is countable, and every element of its transitive closure is countable. If the axiom of countable choice holds, then a set is hereditarily countable if and only if its transitive closure is countable.

So using choice we somehow get "all elements of TC($x$) are countable" from "TC($x$) is countable". How does this work?
HS
A set is $small$ if it can be injected into one of the sets $\omega, \mathcal P\omega, \mathcal P\mathcal P\omega, \ldots$
Again we have empty-set, pair-set, union. Power-set also holds as we can inject $\mathcal Px$ into $\mathcal P^{n+1}\omega$ given $x$ injects into $\mathcal P^n\omega$. Infinity definitely holds as $\omega$ injects into $\omega$. I'm not sure about foundation, separation, and replacement though.
 A: For $HF$: Why do you think you can get $x\in HF$ with $x\in x$? Do you have an example? (HINT: every set in $HF$ is a set in "the universe," which satisfies foundation . . .)
As to Separation and Replacement: Remember that each of these axioms (rather, each axiom in each of these schemes) takes a "starting" set $X$ and constructs a "new" set $Y$ (OK yes this is sloppy, but the intuition is right). How does the size of the new set compare to the size of the starting set? Do you see why this implies that you can't leave $HF$ via Separation and Replacement?
For $HC$: The role of choice is in making countable unions of countable sets countable. In principle, it is possible to have a countable set of countable sets, $A=\{A_n: n\in\omega\}$, whose union $\bigcup A$ is not countable. This has been treated repeatedly on this site, so I won't say much more here. Note that the implication you mention - "If $TC(x)$ is countable, then each element of $TC(x)$ is countable" - actually requires no choice at all, since every element of $TC(x)$ is also a subset of $TC(x)$; it's the converse, "If each element of $TC(x)$ is countable, then $TC(x)$ is countable", which is problematic.
For $HS$: This is more complicated, and really gets to the meat of what Replacement means. HINT: Can you think of a collection of things in $HS$ which is "small" (e.g. has size = something in $HS$) but "unbounded" (e.g. not contained in anything in $HS$)? Think about "climbing up" $HS$ somehow . . .
(As for Separation in $HS$: are you familiar with the cumulative hierarchy? If so, do you see why Separation cannot yield sets of higher rank, and why $HS$ is an initial segment of the cumulative hierarchy?)
