$\textbf{Logic:}$ Mono-sorted first order logic with equality.
$\textbf{Extralogical Primitives: } <, \in$
Define: $x > y \iff y < x$
Define: $x \leq y \iff x < y \lor x=y$
$ \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$
(I hope the degenerate case present in the answer to an earlier formulation is avoided here).
Call this theory $T$, so $T$ 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.
Now, according to a comment by Emil Jeřábek on being able to extend $T$ with the following axiom:
- $\textbf {Parallel:} \ y \in x \to y < x$
, which would prove all axioms of $\sf ZF_{fin}$ which would be a fragment of $T+\sf Parallel$. So an extension of $T$ has a fragment of it that is synonymous with $\sf PA$, and per that comment this is seen to be a feature of $T$ being trustworthy! Now, I'll assume that $\sf PA$ is trustworthy, so we must be able to extend it into a theory ${\sf PA}'$ such that a fragment of it would be synonymous with $T$. And so this provides the basis for the following questions:
Which theory in the language of $\sf PA$ is synonymous with $T$?
Which fragment of a set theory extending $\sf ZF_{fin}$ is synonymous with $T$?
