Language: Mono-sorted first order logic with equality.

Extralogical Primitives: $<, \in$

Define: $x \leq y \iff x < y \lor x=y$

• $\textbf{Well ordering: }\\\textit{Transitive:} \ x < y \land y < z \to x < z \\ \textit{Connective:} \ x \neq y \leftrightarrow (x < y \lor y < x) \\ \textit{Well founded:} \ \exists n \in x \to \exists n \in x \forall m \in x (n \leq m)$

• $\textbf{Finiteness: }\exists n \in x \to \exists n \in x \forall m \in x (m \leq n)$

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

Is this theory synonymous with $\sf PA$?