$\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?"][1], and as shown per answers, it is [not bi-interpretable][2] with $\sf PA$, though it is [mutually interpretable][3] 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? 
    


  [1]: https://mathoverflow.net/q/461599/95347
  [2]: https://mathoverflow.net/a/461632/95347
  [3]: https://mathoverflow.net/a/461626/95347