Model theorists have a lot to say about so-called definable imaginary elements of a structure. One way to formulate imaginaries is the following: Suppose $\M$$\mathcal{M}$ is a structure with universe $M$, and let $G$ be the automorphism group of \M$\mathcal{M}$. Define V_0(M) = M, V_{\alpha+1}(M) = V_\alpha\cup P(V_\alpha(M)), V_\lambda = \bigcup_{\alpha<\lambda}V__\alpha(M) when \lambda $$V_0(M) = M, \quad V_{\alpha+1}(M) = V_\alpha\cup P(V_\alpha(M)), \quad V_\lambda = \bigcup_{\alpha<\lambda}V_\alpha(M)$$ when $\lambda$ is a limit ordinal. Let V(M) = \bigcup_{\alpha<\infty}V__\alpha(M). Then G $$V(M) = \bigcup_{\alpha<\infty}V_\alpha(M).$$ Then $G$ has a natural action on $V(M)$ defined inductively by g(x) = $$g(x) = \{g(y):y\in x\}.$$ If {g(y):y\in x}. If x\in V(M)$x\in V(M)$ and S\subseteq M$S\subseteq M$, then S$S$ supports x$x$ if G(S)\subseteq G({x})$G(S)\subseteq G(\{x\})$, where G(S)$G(S)$ is the pointwise stabilizer of S$S$ and G({x})$G(\{x\})$ is the setwise stabilizer of x$x$. The imaginaries are those x\in V(M)$x\in V(M)$ which have finite support.
Now, for a finite structure \M$\mathcal{M}$, it makes sense to work with HF(M)$HF(M)$ instead of V(M) $V(M)$ (stop the construction at the first countable infinite ordinal).
I would like to know if anyone has done any work regarding the action of a group of permutations of a finite set X$X$ on the hereditarily finite sets above X$X$. Ideally, I'd like to get results "off the shelf" if they're out there.
