Can $\mathsf{TNT}$ be modeled in non-well-founded models of $\mathsf{ZF}$? The theory $\mathsf{TNT}$, introduced by Hao Wang in 1952, adds negative types to simple Type Set Theory $\mathsf{TST}$, so it's written exactly as $\mathsf{TST}$ but with the type indices ranging over $\mathbb Z$ instead of just $\mathbb N$.
Let $\mathsf{ZF}\text{-Reg.}$ be the milieu for models, let $M$ be a transitive non-well-founded model of $\mathsf{ZF}$, by that I mean $(M, \in_M)$ where $\in_M$ is not well founded. So as seen from the outside of $M$, there must exist a non-standard infinite ordinal $\zeta$ such that there exists an infinite descending sequence $V_\zeta, V_{\zeta-1}, V_{\zeta-2},\dotsc$ of stages of $\mathsf{ZF}$. Now, take $\mathcal M = \displaystyle\bigcup_{n \in \mathbb N} V_{\zeta \ \pm \ n}$ :

Can this this provide a model of $\mathsf{TNT}$, where each sort $i$ range over $V_{\zeta + i}$, and the membership relation from sort $i$ to sort $i+1$ is the membership relation restricted to $V_{\zeta+i} \times V_{\zeta + i + 1}$?


Can we have an omega model this way? I mean the set of naturals in $\mathcal M$ is standard, i.e. externally well-founded finite von Neumann ordinals. Which (if it models $\mathsf{TNT}$) is known to violate $\mathsf{AC}$.

 A: Per comments, the above conditions might not be enough to ensure the result of interpreting $\sf TNT$, however, the following line would work to answer the first quetion:
Suppose we work in $\sf ZF−Reg.$ on a transitive non-$\omega$-non-well-founded model $M$ of $\sf Finite \ \sf ZF$ (i.e. $\sf ZF -\text{ inf.+ every set is finite}$), so the rank of every nonempty set must be a successor rank, now since its non-well-founded then there must exist a non-standard ordinal, i.e. internally looks like a finite von Neumann ordinal but externally it has an infinite predecessor chain subset of it, now working externally [in $\sf ZF-Reg.$] since $M$ is just a set, then pick any such ordinal $\zeta$ and send $V_\zeta$ to $0$, then send its predecessor stage to $\mathbb N \setminus 1 $ (which captures the integer $−1$), and the predecessor stage of that to $\mathbb N \setminus 2 $, etc...; send each $V_{\zeta +n}$ to $n$ for each $n \in \mathbb N$. Notice that $\mathbb N$ is the set of all standard naturals in $M$. It's easy to define the restrictions on membership relations, the types are the stages of $M$ that are the preimages of the intergers under the above assignment, and the rest goes through easily.
