Add a primitive total one place fuction symbol $\tau$, and a primitive binary relation $<$, to the language of set theory. Add the following axioms:
Extensionality: $\forall z \, (z \in x \iff z\in y) \implies x=y$
Sets with the same elements, are equal.
Define: $\alpha \text { is a type } \iff \exists x: \alpha=\tau(x) $
We will restrict Greek letters for types.
Types: $ {\sf Transitive \! : } \ \alpha < \beta < \gamma \implies \alpha < \gamma \\ {\sf Connected\!: } \ \alpha \neq \beta \iff \alpha < \beta \lor \beta < \alpha \\ {\sf well \ founded\!: } \ \phi(\alpha) \implies \exists \beta: \phi(\beta) \land \\\forall \alpha (\phi(\alpha) \implies \alpha \not < \beta) \\ {\sf Increment\!: }\ \forall \alpha \, \exists \beta: \alpha < \beta \\ {\sf Infinity\!: } \ \exists \lambda \neq 0: \forall \alpha < \lambda \, \exists \beta: \alpha < \beta < \lambda$
Typing: $ \forall y \in x\, (\tau(y) < \tau(k)) \iff \tau(x) \leq \tau(k)$
The type of a set is the limit to the type of its elements.
Predicative typed comprehension: $$ \forall \alpha \forall x_1,\dotsc,\forall x_n: \\ (\underset {i=1} {\overset {n} \bigwedge}\tau(x_i) < \alpha) \land \lim \tau ``\phi^\alpha =\alpha \\\implies \exists x \ \forall y \ (y \in x \iff \phi^\alpha);$$ where $\phi^\alpha$ is a formula having all of its quantifiers of the forms $$\forall k \, (\tau(k) < \alpha \implies \dots); \\\exists k (\tau(k) < \alpha \, \land \dots)$$, and its free variables are $y,x_1,\dotsc,x_n$, and $$\lim \tau``\phi =\alpha \iff \\\forall \zeta (\forall y (\phi \implies \tau(y) < \zeta) \iff \alpha \leq \zeta).$$
In English: for a type $\alpha$ if the limit to the type of all objects that a formula $\phi$ holds of is $\alpha$, and if the type of all variables (bound and free) in $\phi$ is strictly lower than $\alpha$, then $\phi$ defines a set.
Countability: Every set is countable.
Choice: Every set is well orderable.
Can this theory interpret $\sf PA$?
If we allow some impredicativity by replacing $\leq$ instead of $<$ in the quantifier and the free variable restrictions of the comprehension schema, and remove the countability axiom; would that increase the consistency strength to at least ${\sf Z}_2$?
