To which arithmetic\set theory this theory is bi-interpretable?

Question

$\textbf{Logic:}$ Mono-sorted first order logic with equality.

$\textbf{Extralogical Primitives: } <, \in$

$ \textbf{Axioms:}$

• $ \textbf{Order:} \ x < y < z \to x < z $

• $ \textbf{Finiteness:} \\ y \in x \to \exists \, l,u \in x \forall m \in x : m \neq l \leftrightarrow l < m \leq u $

• $\textbf{Sets: } \forall n \exists! x \forall m (m \in x \leftrightarrow n \not < m \land \phi)$, if $x$ is not free in formula $\phi$.

This theory is just a reformulation of the theory presented in posting titled "Is this theory synonymous with PA?", and as shown per answers, it is not bi-interpretable with $\sf PA$, though it is mutually interpretable with it.

Two questions:

To which theory in the language of $\sf PA$ this theory is bi-interpretable?

To which fragment of the standard set theory this theory is bi-interpretable?

Answer 1

Your theory is true in the one-element universe $\{a\}$ in which $a<a$ is true and $a\in a$ is false. The order transitivity holds trivially in this case; the finiteness axiom holds vacuously; and the sets axiom holds, since the LHS and RHS of the biconditional are both false, and there is a unique $x$, since $x=a$ is the only object available.

So it seems that this theory does not necessarily express any interesting version of set theory.