Here is a model of your "finite set theory" (including Foundation) in which there is an infinite set and Power Set and Replacement fail. Let $A=\{\emptyset,\{\emptyset\},\{\{\emptyset\}\},\{\{\{\emptyset\}\}\},\dots\}$ and let $M$ be the closure of $V_\omega\cup\{A\}$ under Pairing, Union, and taking subsets (so if $X\in M$ and $Y\subseteq X$ then $Y\in M$). It is clear that $M$ satisfies all of your axioms except possibly the negation of Infinity. To prove the negation of Infinity, note that if $X\in M$, then the transitive closure of $X$ contains only finitely many elements of cardinality $>1$ (since this is true of $A$ and for every element of $V_\omega$, and is preserved by taking pairs, unions, and subsets). So $M$ cannot contain any inductive set.
However, $M$ does contain an infinite set, namely $A$. It is also clear that $M$ fails to satisfy Power Set, since $M$ contains every subset of $A$ but $\mathcal{P}(A)\not\in M$ (either by the criterion mentioned above, or by noting that every element of $M$ is countable). Replacement also fails, since the usual recursive definition of the obvious bijection $A\to\omega$ can be implemented in $M$, so Replacement would imply $\omega$ is a set.
This model does satisfy Choice in the form "if $X$ is a set of disjoint nonempty sets then there is a set that contains one element from each of them" (since $M$ contains all subsets of $\bigcup X$). It does not satisfy Choice in the form "if $X$ is a set of nonempty sets then there exists a choice function $X\to\bigcup X$", basically because it is very hard to construct functions as sets in $M$ (for instance, if $X=A\setminus\{\emptyset\}$, the unique choice function for $X$ would have infinitely many 2-element sets in its transitive closure). Probably it is possible to build a model where any reasonable form of Choice fails, but I don't know how exactly to do that at the moment.
This is because the framework described by the NBG axioms is strictly richer than that which the ZFC axioms describe. This is not an isolated phenomenon. Let me show you diffrent, perhaps a bit less abstract examples.
First example.
It is a well-known consequence of compactness that there is no first-order axiom in the language with just equality whose models are exactly the infinite sets. We need infinitely many axioms saying that there are at least $n$ elements, for arbitrarily large $n$.
On the other hand, if we add a linear ordering, we can consider the theory of dense linear orderings (with at least two points), which is finitely axiomatisable and has no finite models.
Every infinite set can be expanded to a dense linear ordering. Thus, the pure sets underlying dense linear orderings are exactly all infinite sets.
Second example.
For a field $F=(F,+,\cdot,0,1)$, the following are equivalent:
- $F$ is formally real, i.e. whenever a sum of squares is zero, all of them have to be zero.
- There is a linear ordering $\leq$ on $F$ which is compatible with the field operations (making $(F,+,\cdot,0,1,\leq)$ an ordered field).
Now, the first order of formally real fields is not finitely axiomatisable: for any $n$, there is a field which is not formally real, but such that the sum of at most $n$ squares, not all zero, is necessarily nonzero. The conclusion follows by compactness.
On the other hand, the theory of ordered fields is obviously finitely axiomatisable.
In this case, the pure fields described by the (finitely axiomatisable) theory of ordered fields are exactly the same as the pure fields described by the (not finitely axiomatisable) theory of formally real fields.
In both examples, the extra structure provided by the linear ordering allows us to force infinitely many axioms to hold simultaneously. Similarly, for NBG, the extra structure provided by the addition of proper classes as elements allows us to force infinitely many axioms to hold simultaneously.
In all cases, the cost is that we need to choose this extra structure: there are many ways to choose a dense linear ordering of an infinite sets, there are (typically) many ways to choose a compatible linear ordering for a formally real field, and there are also (typically?) many ways to expand a model of ZFC to a model of NBG - a pure set does not know its dense linear orderings, a formally real field (usually) does not know any particular compatible ordering, and there is no reason for a model of ZFC to know what classes you should endow it with to get a model of NBG.
Best Answer
In my experience, "NBG" doesn't necessarily mean global choice... oftentimes it does, but conventions vary. So it's good form to be explicit. So you could just say "NBG with local choice".
However, that's assuming that, choice aside, this is NBG. The last two axioms I've never heard of, but I'll just assume they are innocuous quirks of the presentation.
(edit: I looked it up and they are unnecessary axioms the author introduces on a provisional basis before proving.)
The main issue has to do with axiom A2. Are the formulas for class construction restricted so that you can't quantify over proper classes? If not, then you aren't dealing with an NBG-like theory, but rather a Morse-Kelley-like one.
(edit: I could be mistaken cause the presentation of logic is too long for me to read right now, but it doesn't look like the author is making this restriction. So seems like Morse-Kelley. Although it’s possible the author never uses the stronger comprehension instances so is effectively working in NBG.)