The axiom of pairing uses "objects" $a$ and $b$ to form the set $\{a,b\}$, and the objects in this case can be either individuals or sets. But it seems to me that the entire point of the axioms is to establish what a set is, so how can we use the concept of a set in its definition?
In set theory, is the axiom of pairing circular
set-theory
Related Solutions
You have $x,y$, let us construct the pair $\{x,y\}$.
First note that $\varnothing=\{z\in x\mid z\neq z\}$. So we have the empty set. Now by the power set axiom we have $P(\varnothing)=\{\varnothing\}$ and $P(P(\varnothing))=\{\varnothing,\{\varnothing\}\}$.
Now let us define a formula (with parameters $x,y$):
$$\varphi(u,v,x,y)\colon= (u=\varnothing\land v=x)\lor(u=\{\varnothing\}\land v=y\})$$
(Note that $\{\varnothing\}$ can be defined explicitly as the set that all its elements are the empty sets)
Using replacement now, we set the parameters $x,y$ now the axiom says that $\{u\mid\exists v\in P(P(\varnothing))\colon\varphi(v,u,x,y)\}$ exists. But this set is exactly $\{x,y\}$.
You cannot use the axiom of union to prove from the existence of $\{x\}$ and $\{y\}$ the existence of the set $\{x,y\}$. The axiom of union says that if $A$ is a set then $\bigcup A$ is a set. However you want to say that $\{\{x\},\{y\}\}$ is a set therefore its union, which is $\{x,y\}$ is a set. You already assume the existence of a pair.
You can indeed use separation to prove the existence of $\{x\}$ using the power set axiom as well.
To use a power set, or separation argument you have already the existence of some set. Note that the power set axiom says that if $x$ is a set then there exists a set which contains all the subsets of $x$. Separation is the same, you assume the existence of a set. If you wish to use these two, adding an assumption that an empty set exists is meaningless (note that empty sets exists due to separation, so using it for $\{x\}$ is the same as using it for $\varnothing$).
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.
Best Answer
First, the purpose of the axioms of set theory is not to tell us what a set is. This is a fundamentally philosophical question. The axioms’ purpose is to tell us some facts about how sets relate to each other (and, if we allow things that aren’t sets in our theory, how sets relate to these other things).
Second, when studying set theory, one traditionally works in a theory where everything is a set, such as ZFC. This is certainly not required; people often study the set theory ZFA, which stipulates the existence of a set of “atoms”, where the atoms are not sets. But it is customary to study ZFC-like theories, for better or worse. This is why you will see people comment that your distinction between “individuals” and “sets” is not meaningful.