# 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}$$.

• @LSpice, thanks! Jul 22, 2022 at 19:52
• Your claim about $\zeta$ is not true: all we can say is that there are $M$-ordinals $\zeta_i$ ($i$ a (true) natural number) such that $\zeta_0>\zeta_1>...$ - we need not have $\zeta_{i+1}+1=\zeta_i$. In particular, if $M$ is an ill-founded $\omega$-model, no such chain will exist. Jul 22, 2022 at 20:12
• @NoahSchweber, you mean $\zeta_{i-1} +1 = \zeta_i$. Jul 22, 2022 at 20:35
• No, I don't: note that as indices increase, my $\zeta$s decrease. So $\zeta_{i+1}$ should be smaller than $\zeta_i$. Jul 22, 2022 at 20:36
• @NoahSchweber, is there a result that this cannot be done, I mean its always the case that the $\zeta_i$'s are not immediate predecessor chains. Jul 22, 2022 at 21:19

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.