Language: mono-sorted first order language of set theory with a new primitive total unary function symbol $\tau$, denoting the type of sets, and a primitive binary relation $<$.
Define: $x \leq y \equiv_{\sf df} x < y \lor x=y$
Extensionality: as in NFU.
Type axioms:
$\tau(\tau(x))=\tau(x) \\ \tau(x) \not < \tau(x) \\ \tau(x) < \tau(y) < \tau(z) \to \tau(x) < \tau(z) \\ \exists x: \phi(x), \to \exists x: \phi(x) \land \forall y (\phi(y) \to \tau(x) \leq \tau(y)) \\\tau(x) = \lim \tau(y): y \in x$
Where "$\lim$" is strict. So the last axiom is saying that the type of every set is the minimal type strictly larger than all types of its elements.
Notation: $\phi^\alpha$ is a formula that results from formula $\phi$ in FOL($=,\in$) by bounding its quantifiers to types strictly less than $\alpha$, i.e. quantifiers become of the forms $(\forall x: \tau(x)<\alpha \to \ldots; \exists x: \tau(x)<\alpha \land \ldots) $.
- Predicative Comprehension: $ \tau(x_1) < \alpha,\ldots, \tau(x_n) < \alpha \\\lim \tau(y)\phi^\alpha (y) = \alpha \to \exists x \forall y (y \in x \leftrightarrow \phi^\alpha(y)) $
We denote types by naturals, so the bottom type is $0$, i.e. the type of empty objects, the next is $1$ and so on... While $T_n$ for a natural $n$ is the set of all objects of type $n$.
Impredicativity axioms:
Union: $\tau(x) < 4 \to \exists y: y= \bigcup x$
Bijection: $\exists f: f \text { is 1-0 bijective}$
Imaging: $f \text { is 1-0 bijective } \land \tau(x) < 4 \\\to f[x], f^{-1}[x], f^2[x] \text { exist } $
Where, $f[x]=\{f(y): y \in x \}; f^2[x]= \{f[y]: y \in x\}$
An unordered bijection from $X$ to $Y$ is a set of unordered pairs $\{x,y\}$ where $x \in X, y \in Y$, where the pairing of $x$ to $y$ by those pairs follows a one-to-one correspondence. If $f$ is such a bijection from $T_1$ to $T_0$, we call it $\text {1-0 bijective}$.
Is there a clear inconsistency argument for the above system?
The idea is that the system generally follows tenets of predicativism, but with violations to it allowed just for the lower four levels. Now, it is known that if we add set unions or imaging, over all levels then this clearly breaks predicativity and so we'll have a full impredicative theory. But here it is about having minimal violations to it up to some level, so there is a non-strict upper bound on impredicativity which is at subsets of $T_2$.
The real question is does having an upper bound on impredicativity allows for a break of Cantor's theorem as to permit a bijection between a set and its powerset below that bound.
Technically, what's going on here is that $f$ being a $\text {1-0}$ bijection is a type 3 set, i.e. a subset of $T_2$. And predicative comprehension doesn't allow construction of sets of a type that is not bigger than the type of the parameters. Now, the class of all elements of $T_0$ that are not in their preimages under that $f$, call those elements as the culprit elements, is not granted by predicative comprehension because it would be of type 1. Now, one can use unions or imaging to get sets of lower type, but this is not allowed for type 4 sets. So, suppose we use comprehension to get the set of all iterative singletons of the culprit elements, we need to iterate the singleton operator over them at least 3 times, so the set of all these iterative singletons would be a type 4 set, then we cannot use union or images to construct downwardly the diagonal set, i.e. the set of the culprit elements of $T_0$.
So, it seems that seasoning a predicative system with limited kind of impredicativity doesn't enact full impredicativity, which may leave some room for violating Cantor's theorem, and thereby getting bijections between sets and their powersets. But, this may not be true, hence the question.
