Let $M$ be some non-well-founded model of $\sf ZF$, can we have a sequence $(S\_n)\_{n \in \mathbb N}$ of nonempty sets in $M$, where each $S\_n \subset \mathcal P(S\_{n+1})$; and such that there exists a sequence of bijective functions $(f\_n)\_{n \in \mathbb N}: S\_{n+1} \to S\_n$, having : $f\_n(x) = f\_{n+1}[x]$?


This can work in $\sf ZF-Reg.$ like singleton maps "$x \mapsto \{x\}$" between sets of iterated singletons. But here $M$ satisfies Foundation.



Can we have such an infinite descending sequence of functions with prior ones inside their successors?
(Note that I am assuming the axiom of choice in the metatheory. If you want to ask if this holds without choice, clarify and add the appropriate tag. I suspect that this particular compactness instance should be true even without choice, but I am not an expert, nor did I think much about it.)


This is true by a standard compactness argument (assuming ZF is consistent). You can even demand that each $S\_n$ be singleton.


Namely, fixing an arbitrary model $M$ of ZF, the set $\{x\_n=\{x\_{n+1}\}\mid n\in \mathbf N\}^\dagger$ is a type in $M$ in variables $(x\_n)\_{n\in\mathbf N}$ (clearly, every finite part is realised in $M$), so there is an elementary extension $N\succeq M$ in which it is realised. In particular, $N$ is a model of ZF (in fact, of the theory of $M$) with the sequences you wanted.


$\dagger$: naturally, here, $x\_n=\{x\_{n+1}\}$ is short for $x\_{n+1}\in x\_n\land\forall y(y\in x\_n\rightarrow y=x\_{n+1})$


