Proving the Powerset Axiom for hereditarily finite sets 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.
 A: Here is my attempt. Any suggestion or correction will be welcomed.
Negation of the axiom of infinity states that every set has finite cardinality. Thus we may apply the induction for cardinal of sets.
The technical problem that arises is we can use the induction though we does not have the power set axiom. Fortunately, proving induction just needs the well-order property of class of all ordinals so absence of power set is irrelevant.
Let $x$ be arbitrary set and $n=|x|$. If $n=0$ then $x=\varnothing$ and we can check that there is a powet set of $\varnothing$, namely $\{\varnothing\}$. It is a consequence of the pairing. If the statement holds for $n$ and $y$ be a set such that $|y|=n+1$, Since $y$ is nonempty we have some $a\in y$. By inductive hypothesis, we have a power set $\mathcal{P}(y-\{a\})$ of $y-\{a\}$. Axiom of replacement and the axiom of union enables to define the set
$$z := \mathcal{P}(y-\{a\}) \cup\{t\cup\{a\} \mid t\in \mathcal{P}(y-\{a\})\,\}.$$
We can check that $z$ is a power set of $y$. Therefore by induction the axiom of power set follows.
A: Let me denote $ZF^{¬\infty}$ to be the axioms of $ZF$ with the axiom of infinity replaced by its negation.
Before going into anything else, it is worth pointing out that (if $ZF$ is consistent) then $ZF^{¬\infty}$ has many different models, not just $V_\omega$. This is because without infinity, the axiom of foundation becomes significantly weaker. To see this - consider the following two statements:


*

*The Axiom of Foundation (Fo): If $X$ is a set, then there exists $y \in X$ with $y \cap X = \emptyset$.

*The Von Neumann Rank Axiom (VNR): If $X$ is a set, then there exists an ordinal $\alpha$ with $X \subseteq V_\alpha$.
In $(ZF - Fo)$ these two axioms are equivalent, but this equivalence brakes down in the absence of infinity. There are models of $ZF^{¬\infty}$ where VNR fails, and such an example can be seen here.

As a side note, the claim that "$V_\omega$ is the universe of sets" is equivalent to VRN with respect to $ZF^{¬\infty},$ or in other words $ZF^{¬\infty} \vDash ($VNR $\iff$ "$V_\omega$ is the universe of sets"$)$.
VNR is a very powerful strengthening of foundation with respect to $ZF^{¬\infty}$. If we denote:


*

*$T = (ZF^{¬\infty} + VNR) - ($"the axiom of replacement/separation" and "the power set axiom"$)$


then $T$ is powerful enough to prove all three of these missing axioms - and also the axiom of choice. We can see this as follows:


*

*Given that $X$ is a set, and $\phi$ is a class-function. Then there exists a natural number $n$ with $X \subseteq V_n$, and we can prove by induction that $|V_n|$ is finite - and therefore |X| is finite. This means that the class $Y = \{y : \exists x \in X(\phi(x) = y) \}$ is finite.
The rank of each $y \in Y$ (the smallest $m$ such that $y \subseteq V_m$) is finite as $Y \subseteq V_\omega$, and $rank(Y) = \sup\{rank(y) : y \in Y\}$. This means that $rank(Y)$ is finite (as it is the supremum of a finite amount of natural numbers), and therefore there exists a natural number $N$ with $Y \subseteq V_N$ - so that $Y \in V_\omega$ and therefore $Y$ is a set.
This proves the axiom of replacement, as $X$ and $\phi$ are arbitrary.

*The axiom of separation follows trivially from the axiom of replacement and the empty set axiom.

*Given that $X$ is a set. Then there exists a natural number $n$ with $X \subseteq V_n$. Then we have the set $P_X = \{Y \in V_{n+1} : Y \subseteq X \}$ via the axiom of separation, and moreover $P_X$ qualifies as being the power set of $X$. This proves the power set axiom, as $X$ is arbitrary.

*Given that $X$ is a set. Then there exists a natural number $n$ with $X \subseteq V_n$. Note that by induction we can construct a bijection $f_n \colon V_n \to {^{n-1}2}$, and then $f_n$ restricts to an injection $f_n |_X \colon X \to {^{n-1}2}$. (Side note, we define ${^{-1}2} = 0$ and ${^{m+1}2} = 2^{(^{m}2)}$).
This allows us to well-order $X$ via $x \leq y$ if and only if $f_n|_X(x) \leq f_n|_X(y)$, which proves the well-ordering theorem (and therefore the axiom of choice) as $X$ is arbitrary.

This shows us the power of the axiom system $T$ where we had strengthened the axiom of foundation to satisfy VNR. However without VNR we don't have such luxury.


*

*The example from the beginning gives us a model of $ZF^{¬\infty}$ that satisfies the negation of choice.

*Define $S = ZF^{¬\infty} - ($"the axiom of replacement" and "the power set axiom"$)$. Then it can be shown that $S \vDash ($"the power set axiom"$ \implies $"the axiom of replacement"$)$.
This is because in $S$, the power set axiom holds if and only if there are no infinite sets - and finite classes are always sets via the axiom of pairs and the axiom of unions.
On the other hand - the reverse implication doesn't hold. For example if we define a set $X$ to be pseudo-finite iff $X, \bigcup X, \bigcup \bigcup X, ...$ are all Dedekind-finite - then for any model $M$ of $ZF$, we have that $P = \{x \in M : x$ is pseudo-finite$\}$ is always a model of $S$ and satisfies the axiom of replacement.
So simply take $M$ to be a model of $ZF$ that contains an infinite pseudo-finite set, and we have our example.

*As for a model of $S$ that satisfies both the negation of the power set axiom and the negation the axiom of replacement, start with some infinite pseudo-finite set $A$. Then define the following sets:


*

*$B_0 = V_\omega \cup A \cup \{A\}$.

*$B_{2n+1}$ is the closure of $B_{2n}$ under pairs and unions, for $n \in \mathbb{N}$.

*$B_{2n+2}$ is the set of all sets obtainable from $B_{2n+1}$ via the axiom of separation, for $n \in \mathbb{N}$.



Then $B = \bigcup_{n \in \mathbb{N}} B_n$ is a model of $S$ and satisfies the negation of the power set axiom, yet the class $\{ \{A,a\} : a \in A\}$ cannot be a set in $B$ despite being definable via a class-function from $A$.
Hence $B$ is a model of $S$ that satisfies both the negation of the power set axiom and the negation of the axiom of replacement.
A: 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.
