The theory $\mathsf{TNT}$, introduced by Hao Wang in 1952, adds negative types to simple [Type Set Theory $\mathsf{TST}$](https://en.wikipedia.org/wiki/New_Foundations#The_Type_Theory_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}$.
> 
> 
> 



Can $\mathsf{TNT}$ be modeled in non-well-founded models of $\mathsf{ZF}$?
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.


