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$?