Satisfaction of theories like "second-order" arithmetic by models with "converse" comprehension I fix a two-sorted language $L$ like that of "second-order" arithmetic.  That is, an $L$-structure $M$ is a disjoint union $M = N \sqcup S$ of the domains of the two sorts with an interpretation $\mathord{\in^M} \subseteq N \times S$ of $\in$. The language $L$ may have other symbols.  Now there is an $L$-theory $T_0$ that expresses comprehension and extensionality, and every model of $T_0$ is isomorphic to the disjoint union of $N$ and a family of subsets of $N$ where $\in$ is interpreted as the set-theoretic membership.
Let $T$ be a consistent extension of $T_0$.  My question is whether $T$ has a model $M$ that satisfies the "converse" of comprehension, somewhat like Goedel's constructive universe.  That is, I would like a model $M = N \sqcup S$ of $T$ such that every element $X \in S$ is equal to $\phi(M)$ for some formula $\phi(x) \in L(N)$ where $x$ is a variable for the first sort. (For some reason, I don't care about formulas with parameters from the second sort.)
Has this appeared somewhere?
 A: No.  For instance, suppose the language has just one other symbol, a function $f:N\to N$.  Let $X=\{0,1\}\times\mathbb{N}$ and let $T$ be the complete theory of the structure $X\sqcup\mathcal{P}(X)$ where $f:X\to X$ is given by $f(x,y)=(1-x,y)$.  In particular, $T$ includes the statement that there exists $A\in S$ such that $N$ is the disjoint union of $A$ and $f(A)$ (for instance, $A=\{0\}\times\mathbb{N}$).  However, I claim no such set $A$ can be definable with parameters from $N$ in any model $M$ of $T$.
To prove this, note that given any finite set of parameters in $N$ (which we may assume is closed under $f$), there is an automorphism $g$ of $M$ fixing the parameters induced by the map which fixes the parameters but is given by $f$ on the rest of $N$ (and given on $S$ by the induced map on subsets; note that $S$ must be closed under this induced map since $g$ is definable).  Any set $A\subseteq N$ definable using these parameters must then be fixed by $g$.  Since $N$ must have orbits of $f$ that are not in our finite set of parameters, this means that $N$ cannot be the disjoint union of $A$ and $f(A)$.
(In fact, by also considering automorphisms which fix all the parameters and swap an arbitrary pair of other orbits of $f$, we can conclude that any subset of $N$ definable with parameters from $N$ must be finite or cofinite.)
