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

4more comments