Finite Set Induction Let A be a set and let $FS(A)$ be the set of all finite subsets of $A$. Then to prove a formula of the form
$$(\forall S \in FS(A))(Q(S))$$
it is sufficiently to prove the following two formulae:


*

*$Q(\emptyset)$; (the basis of induction)

*$(\forall S \in FS(A), x \in A)(Q(S) \rightarrow Q(S \cup \{x\}))$. (the inductive step)
Does this induction principle have a special name? Maybe, Finite Set Induction?
If it has a name, please provide a reference to the first use.
 A: This is really just induction over a well-founded set.

Definition. We say that $(X,R)$ is a well-founded if whenever $A\subseteq X$ is non-empty, $A$ has an $R$-minimal element.

(Assuming the axiom of choice, this is equivalent to stating that there is no infinite $R$-decreasing sequence in $X$.)
It's not difficult to see that $FS(A)$ is well-founded under $\subseteq$. So we can utilize the following theorem:

Theorem. Suppose that $(X,R)$ is a well-founded partial order, and $\varphi$ is a property such that for every $x\in X$ it holds:
  $$(\forall y(y\mathrel R x\rightarrow\varphi(y)))\rightarrow\varphi(x),$$
  then $\forall x\in X.\varphi(x)$.

Now it's not hard to see that the conditions that you gave are exactly sufficient for this. It's true vacuously for $\varnothing$, being the minimal element. The second condition assures that it holds for the singletons, and so for pairs, and so on and so forth.
There's nothing very special about it. In fact, a lot of times when we use strong induction on the natural numbers, we actually use this sort of induction on a different relation which is well-founded.
For example, consider the usual proof that every natural number is $1$ or it has a prime divisor. The relation $m\mathrel R n\iff m\mid n$ is well-founded, and we really do the induction on that order, rather than on the usual order of the natural numbers.
A: Note a full answer, but here is a proof that is works (by regular induction!):
Base Case: For the empty elements in $FS(A)$ your base case proves that $Q$ holds.
Induction Step: Assume $Q$ holds for elements of $FS(A)$ of cardinality $k$. Select an arbitary element of cardinality $k+1$ called $\eta$. Also, select a random element $x$. Now we take $\eta / \{x\}$ This has cardinality $k$, and therefore $Q$ holds for it. By your induction step, it holds for $\eta$.
$$\blacksquare$$
