Consider $\mathsf{ZF}$, and relace the Axiom of Infinity with its negation. This gives us the theory of hereditarily finite sets. Its universe is $V_\omega$. Intuitively, I feel that I can construct any hereditarily finite set starting from the empty set and using only Pairing and Union. So, my questions are:
- Can I drop the Powerset Axiom and prove it from the remaining axioms?
- Can I prove the Axiom of Choice in this theory?
- Assuming I have an explicit axiom postulating the existence of the empty set, can I drop the Axiom Schema of Separation and prove its every instance from the remaining axioms? The same question about Replacement.
All questions are under the assumption that $\mathsf{ZFC}$ is consistent.
We still have the notion of ordinal within your theory, and the class of ordinals is still well-ordered; it just doesn't contain infinite elements: By the negation of INF, every non-empty ordinal is a successor ordinal. We can biject the class of ordinals with the class of pair sets of ordinals together with a "marked copy" of the ordinals: Let $A$ be a fixed non-ordinal. We map $\emptyset\mapsto \{\emptyset,\emptyset\}=\{\emptyset\}$ and recursively if $\alpha\mapsto\{\beta,\gamma\}$ with $\beta\le \gamma$ then we map $\alpha+1\mapsto\begin{cases}\{\beta,A\},&\beta=\gamma\\\{\beta+1,\gamma\},&\beta<\gamma\end{cases}$, and if $\alpha\mapsto \{\beta,A\}$ we let $\alpha+1\mapsto \{\beta+1,\emptyset\}$. If this class map is clalled $F$, we can now map from the class of ordinals to our universe, by letting $G(\emptyset)=\emptyset$, and recursively $G(\alpha+1)=\begin{cases}\{G(\beta),G(\gamma)\},&F(\alpha)=\{\beta,\gamma\}\\\bigcup G(\beta),&F(\alpha)=\{\beta,A\}.\end{cases}$
Clearly, the image of $G$ is closed under pairing and union and contains $\emptyset$. One can show that $G(\alpha)\subseteq G(\beta)$ implies $\alpha\le \beta$. Also one should be readily able to show that: If $X=G(\alpha)$ and $Y=G(\beta)$ then there exists $\gamma$ such that $G(\gamma)=\{\,Z\cup\{X\}\mid Z\in Y\,\}$. Then the image of $G$ is also closed under power set: $\mathcal P(\emptyset)=\{\emptyset\}=G(1)$ and if $S=G(\alpha)$ is not empty, say $s\in S$, then $S\setminus\{s\}=G(\beta)$ for some $\beta<\alpha$ so that we may assume that we already have $Y:=\mathcal P(S\}\setminus\{s\}$ available and $$\mathcal P(S)=Y\cup \{\,Z\cup\{s\}\mid Z\in Y\,\}$$
However, I do not see how $G$ can be shown to be surjective.