Intersection of iterated powerset in NFU I am interested in the existence of the set $\bigcap_{n \in \mathbb{N}} \mathcal{P}^n(x)$ for any given set $x$, in the context of NFU (New Foundations with Urelements). It seems to me that the comprehension axiom in NFU does not allow to prove that $\bigcap_{n \in \mathbb{N}} \mathcal{P}^n(x)$ exists for any set $x$. On the other hand, it seems to me that the model of NFU described in the SEP article Alternative Axiomatic Set Theories satisfies the property that for every $x$, $\bigcap_{n \in \mathbb{N}} \mathcal{P}^n(x)$ exists. 
Let me informally describe my reasons for believing that in that model, $\bigcap_{n \in \mathbb{N}} \mathcal{P}^n(x)$ exists for every $x$. The model described in the SEP article is defined with the help of a non-standard model of ZFC with an automorphism $j$ that moves rank $\alpha$ to a lower rank. In that case, the $V_\alpha$ of that model of ZFC is a model of NFU, if $\in_{NFU}$ is suitably defined as in the linked article. Under those conditions, the interpretation of $\mathcal{P}(x)$ in the model will be an element of $V_{j(\alpha)+1}$. But then the interpretation of $\mathcal{P}^n(x)$ in the model will be an element of $V_{j(\alpha)+1}$ for any $n \in \mathbb{N}$, so the interpretation of $\bigcap_{n \in \mathbb{N}} \mathcal{P}^n(x)$ in the model will also be an element of $V_{j(\alpha)+1}$, so $\bigcap_{n \in \mathbb{N}} \mathcal{P}^n(x)$ exists according to the model.
I have four interdependent questions:


*

*Is it correct that the statement "for every $x$, the set $\bigcap_{n \in \mathbb{N}} \mathcal{P}^n(x)$ exists" is not provable in NFU? 

*Is my above sketch of the claim that the statement "for every $x$, the set $\bigcap_{n \in \mathbb{N}} \mathcal{P}^n(x)$ exists" could be added to NFU without losing consistency correct?

*If the answer to the second question is "no", are there other known ways to prove that the statement "for every $x$, the set $\bigcap_{n \in \mathbb{N}} \mathcal{P}^n(x)$ exists" could be added to NFU without losing consistency?

*If the answer to the fourth question is "no", is it known that adding "for every $x$, the set $\bigcap_{n \in \mathbb{N}} \mathcal{P}^n(x)$ exists" to NFU leads to an inconsistency?

 A: For the first question, the answer is Yes. Since if that was provable in NFU, then it would interpret NF, by then NFU would prove Infinity, but the negation of infinity is consistent with NFU. 
Not only that suppose that it is provable in NFU, then take $x=V$, then the intersection of all iterative powers of $V$ would be the set of all pure sets, by then this would interpret NF, but if we assume that NFU proves that set to exist, then it would exist in ALL models of NFU, but some models of NFU satisfy choice, and clearly the intersection set of all iterative powers of $V$ is both transitive and pure, and the choice set of any element of it would be also a pure set, so it would be closed under choice, but by then it would satisfy NF + Choice. Which is known to be inconsistent!
However that doesn't prevent some models of NFU to have that intersection set existing in their domains, however all of those models would violate choice.
For the second question, the answer is shown in my comment, you didn't prove the existence of the intersection between all $V_{j^n(a) +n}$ in the original model  in order for you to claim that it is an element of $V_{j(a)+1}$.
For the third question, the answer is unknown yet, because the consistency of NF is not settled yet (although Randall Holmes had presented a proof of it, that is not completely vetted yet), and clearly a positive answer to that question would interpret NF.
For the fourth question. the answer is No
