model theory - Actions of finite permutation groups on hereditarily finite sets.

Well, since there have been no answers in a month, let me at least point out the easy fact that if M is finite, then every set in HF(M),
and indeed, every set in V(M), is imaginary over M.

(I assume here that M is taken as urelements in the
definition of V(M), as I mentioned in my comments to the
question above, since otherwise there are problems with the
action of G on V(M) and even HF(M) being well-defined.)

Theorem. If M is finite, then every object in HF(M),
and indeed every object in V(M), is an imaginary element.

Proof: Since M is finite, we may take S=M. If pi fixes
every element of M, then it is easy to see by transfinite
induction that the action of pi on V(M) is the identity.
Namely, if pi fixes every element of V_alpha(M), then it
clearly also fixes every element of V_{alpha+1}(M). And so
it fixes every element of V(M), including HF(M)=V_omega(M).
QED

OK. What this answer really shows is that the question is not about the imaginaries over M, but rather, about gaining a greater understanding of the actiom of G on V(M). Perhaps it would be helpful to define the parameter-free version of imaiginary, where we might say that X in V(M) is pure
imaginary over M if whenever pi is a permutation of M,
then pi(X)=X, under the induced action of pi on V(M). For
example, the set M itself has this property, as does the
power set P(M), the set {M} and {emptyset,M}, and so on. In
addition, any set whose transitive closure includes no
urelements from M will be pure imaginary. The question would be to characterize the pure-imaginary sets
over M.

This question shares many similarities with the various
forcing arguments showing the consistency of the negation
of the Axiom of Choice. Specifically, in the pre-forcing
days, set theorists built what are called the symmetric
models of set theory, by taking an infinite set of
urelements M and restricting to the elements of V(M) having
finite support. One can show that this is a model of
ZF-with-urelements having no wellordering of M. The forcing
proofs of the consistency of not-AC have exactly the same
flavor, where one adds an infinite set of mutually generic
Cohen reals, and then considers the sets that have names
with finite support over this set. This is precisely how
Cohen produced a model of ZF+not-AC, without urelements.

So one of the good reasons to study the imaginary elements over a set M is that they form a model of the set theory ZF-with-urelements. When M is infinite, however, then there can be no linear order of M in the pure imaginaries, since swapping elements outside the support of this set will not fix the order. In particular, M will not be well-orderable in this model of set theory, and so AC will not hold. For finite M, of course, there are linear orders of M having support M, and one can show that V(M) satisifes ZFC-with-urelements. But if one considers only the collection of pure-imaginaries, as I defined them above, then one will not even get ZF-with-urelements, unless M has only one element, since one will lose the Comprehensive (subset) axiom when there are parameters from M. For example, no proper nonempty subset of M can be pure imaginary. From this perspective, the pure imaginary sets are not so nice as the imaginary sets.