> I can easily construct one; does that change anything?)
I don't think so. The way you have constructed the Sn's allows you to re-use a choice function for one set for all the other sets. But I don't think this is possible in general.
This is the thing that makes it hard. If you don't impose some sort of structure on the Sn's then I think you will have a very hard time constructing a choice function for them. That's the whole point. If you want a choice function for such sets in general you have to just assume that one exists without being able to actually exhibit one. Your assumption may be mathematically valid (because AoC is consistent with ZF), but I submit that a reasonable person might find it a little hinky.
I don't think so. The way you have constructed the Sn's allows you to re-use a choice function for one set for all the other sets. But I don't think this is possible in general.
This is the thing that makes it hard. If you don't impose some sort of structure on the Sn's then I think you will have a very hard time constructing a choice function for them. That's the whole point. If you want a choice function for such sets in general you have to just assume that one exists without being able to actually exhibit one. Your assumption may be mathematically valid (because AoC is consistent with ZF), but I submit that a reasonable person might find it a little hinky.