First of all, for the base case of $ZF^{-\infty}$: as was noted, the set of numbers that can be produced here is the same as the set of all numbers 'born' on finite days in Conway's usual construction. I finally got around to digging through my references and it turns out that none of On Numbers And Games, Winning Ways or Surreal Numbers actually give a full proof that the only numbers born on day $n$ are dyadic rationals. Here's a rough outline of the process (omitting the very basic proofs of the usual properties for addition, inequality, etc. and the obvious restriction to positive numbers, since negatives follow easily) that would go into a proof:
- Prove the Simplicity Theorem: if both $X_L$ and $X_R$ are non-empty, the value of $x = \{X_L|X_R\}$ is the simplest (first-created) value strictly between them. Another version of this is that if $x=\{X_L|X_R\}$ and $Y_L\lt x, Y_R \gt x$ then $x=\{X_L,Y_L|X_R,Y_R\}$. This implies that if the numbers born by day $n$ are $0, x_1, \ldots, x_m$ then the numbers born on day $n+1$ will be just $\{0|x_1\}, \{x_1|x_2\}, \ldots, \{x_{m-1}|x_m\}, \{x_m|\}$ - they fill in the gaps.
- Use this to prove the simplest form of the translation theorem: if $x$ is positive, then $1+x = \{1+X_L|1+X_R\}$. This then implies that the numbers greater than $1$ born on day $n+1$ are $1$ more than the numbers born on day $n$ and lets us restrict attention to the numbers between $0$ and $1$.
- By induction, assume that the numbers between $0$ and $1$ born by day $n$ are the dyadic rationals $t/2^{n-1}, 0\lt t\lt 2^{n-1}$. Consider the gap $(a,a+2^{-(n-1)})$ on day $n$ and the number $x_{new} = \{a|a+2^{-(n-1)}\}$ born on day $n+1$; we know that $x_{new} > a$ and $x_{new} < a+2^{-(n-1)}$. Then $x_{new}+x_{new} = \{a+x_{new}|a+2^{-(n-1)}+x_{new}\}$; the left side is thus greater than $a+a$ and less than $a+a+2^{-(n-1)}$; similarly, the right side is greater than $a+a+2^{(n-1)}$ and less than $a+a+2^{-(n-2)}$. The simplest number in this span is $a+a+2^{-(n-1)}$, and so by the simplicity theorem $x_{new}+x_{new} = a+a+2^{-(n-1)}$ and thus $x_{new} = a+2^{-n}$.
For the $NBG^{-\infty}$ case, things are a bit more subtle. It seems clear that you can't get numbers born on any day $\gt\omega$, because those numbers will involve 'class members' - numbers born on at least day $\omega$, with a proper class on either their left or right side, and proper classes aren't available as members. At first I thought you could get all the numbers born on day $\omega$, but the catch is that class comprehension doesn't give you arbitrary countable sets of hereditarily-finite (surreal) numbers (i.e. dyadics), but only definable sets, and what's definable depends on what your language is. If you restrict to $\{\leq, +\}$ then the (traditional) numbers that you can get are all the rationals; if your language is $\{\leq, +, \times\}$ then you should get all algebraic numbers. Over either language, you'll also get $\omega, -\omega$, and all numbers of the form $d\pm 1/\omega$ for dyadic $d$, since these are defined by cuts of the form $\{d|d+{1\over2}, d+{1\over4}, \ldots\}$ and similar. Proving that these are all the defined numbers seems relatively straightforward: if $X_L$ has a largest member $x_L$ then we must have $\inf(X_R) = x_L$ (otherwise there will be some dyadic rational in the range $(x_L, \inf(X_R)$) and so the value is $x_L+{1\over\omega}$ (as this is the simplest number larger than $x_L$ and smaller than all the $X_R$); the dual statement obviously holds if $X_R$ has a smallest member $x_R$. If neither $X_L$ nor $X_R$ has an extremal member in the appropriate direction, then they must have a shared infimum/supremum; at this point it comes down to showing that the supremum of all the values satisfying some system of linear (respectively polynomial) integer inequalities is a rational, respectively algebraic, number.
In short, we do not need to adopt this as an axiom. But...
If there are sets at all, the axiom of subsets tells us that there is an empty set: If $x$ is a set, then $\{y\in x\mid y\ne y\}$ is a set, and is empty, since there are no elements $y$ of $x$ for which $y\ne y$. The axiom of extensionality then tells us that there is only one such empty set.
So, the issue is whether we can prove that there are any sets. The axiom of infinity tells us that there is a set (which is infinite, or inductive, or whatever formalization you use). But this seems like a terrible overkill to check that there are sets, to postulate that there are infinitely many.
Some people prefer to have an axiom that states that there are sets. Of course, some people then just prefer to have an axiom that states that there is an empty set, so we at once have that there are sets, and avoid having to apply comprehension to check that the empty set exists.
Other people adopt a formalization of first order logic in which we can prove that there are sets. More carefully, most formalizations of logic (certainly the one I prefer) prove as a theorem that the universe of discourse is nonempty. In the context of set theory, this means "there are sets". This is pure logic, before we get to the axioms of set theory. Under this approach, we do not need the axiom that states that there are sets, and the existence of the empty set can be established as explained above.
(The logic proof that there are sets is not particularly illuminating or philosophically significant. Usually, one of the axioms of first order logic is that $\forall x\,(x=x)$. If $\exists x\,(x=x)$ --the formal statement corresponding to "there are sets"-- is false, then $\forall x\,(x\ne x)$. Instantiating, we obtain $x\ne x$, and instantiating the axiom $\forall x\,(x=x)$ we obtain $x=x$, and one of these conclusions is the negation of the other, which is a contradiction. This is not particularly illuminating, because of course we choose our logical axioms and rules of instantiation so that this silly argument can go through, it is not a deep result, and probably we do not gain much insight from it.)
It turns out that yet some others prefer to allow the possibility that there are empty universes of discourse, so their formalization of first order logic is slightly different, and in this case, we have to adopt some axiom to conclude that there is at least one set.
At the end of the day, this is considered a minor matter, more an issue of personal taste than a mathematical question.
Best Answer
This is not true. Consider the set $X=\{\emptyset,\{\emptyset\},\{\{\emptyset\}\},\{\{\{\emptyset\}\}\},\dots\}$. Let $M$ be the closure of $X\cup\{X\}$ under the operations of taking subsets, forming pairs, forming power sets, and taking unions. Then $M$ will be a transitive model of the Extensionality, Pairing, Union, Specification, and Powerset axioms (and also Regularity and Choice), as well as your version of Infinity since there is a non-surjective injection $f:X\to X$ given by $f(x)=\{x\}$. However, I claim that $\omega\not\in M$. To prove this, just note that for every $x\in M$, the transitive closure of $x$ contains only finitely many elements of $\omega$ (since this is true of $X\cup\{X\}$ and is preserved by all the operations we close it under to form $M$).