$\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$.

Correction, to avoid the degenerate case mentioned in Hamkins answer below, the axiom schema of sets must be corrected to the following:

• $\textbf{Sets: } \forall n \exists! x \forall m (m \in x \leftrightarrow (n \not < m \lor m=n) \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?", and as shown per answers, it is not bi-interpretable with $\sf PA$, though it is mutually interpretable 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?

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

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

$\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$.

Correction, to avoid the degenerate case mentioned in Hamkins answer below, the axiom schema of sets must be corrected to the following:

• $\textbf{Sets: } \forall n \exists! x \forall m (m \in x \leftrightarrow (n \not < m \lor m=n) \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?", and as shown per answers, it is not bi-interpretable with $\sf PA$, though it is mutually interpretable 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?