# What's the proof theoretic ordinal of this number-set theory?

I was thinking of defining a number-set theory, that is a theory that uses the primitives of equality, strict smaller than, and set membership, in order to coin a theory that is at least as strong as PA.

Define: $$N(x) \iff \exists y (x < y \lor y < x)$$

Here $$N$$ stands for the predicate number.

Asymmetry:$$x < y \implies y \not < x$$

Transitivity:$$x < y < z \implies x < z$$

Connectedness: $$N(x) \land N(y) \implies [x \neq y \iff (x < y \lor y < x)]$$

Extensionality: $$\forall x \forall y [ \forall z ( z \in x \leftrightarrow z \in y) \implies x=y]$$

Comprehension: $$\exists l \forall y (\phi(y) \land N(y) \to y \leq l) \implies \\\exists x \forall y [y \in x \iff \phi(y) \land \exists z(y \in z)]$$

Membership: $$\forall x (\exists y (x \in y) \iff N(x) \lor \exists a \exists b (N(a) \land N(b) \land x=\{a,b\}))$$

Limits:$$\forall x \exists l \not \in x: N(l) \land \forall k [N(k) \land \not \exists y \in x (k \leq y) \implies l \leq k]$$

Pairs: $$x=\{a,b\} \implies \neg N(x)$$.

This theory is in some sense strange in that it proves existence of infinite sets! Yet it doesn't prove the existence of numbers corresponding to their cardinalities.

This theory should interpret PA over natural numbers, which are numbers that are not greater or equal to a limit number greater than zero.

Now this theory is indeed a fragment of second order arithmetic.

What's the proof theoretic ordinal of it?