The following question is about patterns of synonymy relationships around two theories, $T^+$ and $\sf PA$. 
For purposes of self inclusiveness I'll re-iterate $T$ and its extensions.

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

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

***Define:*** $x > y \iff y < x$

 $ \textbf{Axioms:}$
  
 - $ \textbf{Order:} \  x < y  < z \to x < z \land x  \neq y$

 - $ \textbf{Finiteness:}  \ y \in x \to   \exists \, l,u \in x \forall m \in x :  l \leq m  \leq u    $

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

 - $\begin{align} \textbf{Synonymy: }  & y \in x \to y < x \\ &  \sup(x \setminus y ) < \sup (y \setminus x  ) \to  x < y      \end{align}$

$\leq$ and $\not >$ are defined as usual; and "$\sup$" stands for strict supermum of a set, that is the $<$ minimal object strictly bigger ($>$) than all elements of that set; and "$\setminus$" is the usual notion of set difference. 

Call the theory with the first three axioms $T$. Let $T^+$  be $T$ plus the first axiom of synonymy, and let the whole theory be called $T^{++}$.

We know that all three theories are mutually interpretable with $\sf PA$. Also, we know that neither $T$ nor $T^+$ are bi-interpretable with $\sf PA$.

Now, $T^+$ has a fragment ranging over the whole domain of it that is synonymous with $\sf PA$ and that fragment is $\sf ZF_{fin}$ (see [here][1]). Also $T^+$ has an extension which is $T^{++}$ that is also synonymous with $\sf PA$. 

> Does $\sf PA$ enjoy the same synonymy relationship with $T^+$? That is, does $\sf PA$ have a fragment of it ranging over the whole domain of it that is synonymous with $T^+$, and also have an extension of it that is synonymous with $T^+$?


  [1]: https://mathoverflow.net/a/461632/95347