The following question is about patterns of synonymy between 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 synonymous 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). 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^+$?